equal
deleted
inserted
replaced
35 |
35 |
36 Basis "[| F : A ensures B; A-B : (insert {} CC) |] ==> (A,B) : elt CC F" |
36 Basis "[| F : A ensures B; A-B : (insert {} CC) |] ==> (A,B) : elt CC F" |
37 |
37 |
38 Trans "[| (A,B) : elt CC F; (B,C) : elt CC F |] ==> (A,C) : elt CC F" |
38 Trans "[| (A,B) : elt CC F; (B,C) : elt CC F |] ==> (A,C) : elt CC F" |
39 |
39 |
40 Union "{(A,B) | A. A: S} : Pow (elt CC F) ==> (Union S, B) : elt CC F" |
40 Union "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F" |
41 |
|
42 monos Pow_mono |
|
43 |
41 |
44 |
42 |
45 constdefs |
43 constdefs |
46 |
44 |
47 (*the set of all sets determined by f alone*) |
45 (*the set of all sets determined by f alone*) |