Selected Objects
| def | col | Collection(T) == T  Prop |
| def | col_member | x  c == c(x) |
| def | col_singleton | < x > (y) == y = x T |
| def | col_none | < > (x) == False |
| THM | member_col_none |  T:Type{i'}, x:T. x < >   False |
| def | col_equal | c1 = c2 == x:T. x c1 x c2 |
| THM | col_equal_weakening | c1,c2:Collection(T). c1 = c2  c1 = c2 |
| THM | col_equal_inversion | c1,c2:Collection(T). c1 = c2 c2 = c1 |
| THM | col_equal_transitivity | c1,c2,c3:Collection(T). c1 = c2 c2 = c3 c1 = c3 |
| THM | col_member_functionality | c1,c2:Collection(T), t1,t2:T. t1 = t2 c1 = c2 (t1 c1 t2 c2) |
| def | col_le | c1  c2 == x:T. x c1 x c2 |
| THM | col_none_le | c:Collection(T). < > c |
| THM | col_le_weakening | c1,c2:Collection(T). c1 = c2 c1 c2 |
| THM | col_le_transitivity | a,b,c:Collection(T). a b b c a c |
| THM | col_equal_functionality | a1,b1,a2,b2:Collection(T). a1 = b1 a2 = b2 (a1 = a2 b1 = b2) |
| def | col_filter | < x c | P(x) > (x) == x c & P(x) |
| THM | member_col_filter | f:(TProp), c:Collection(T), x:T. x < i c | f(i) > x c & f(x) |
| THM | col_le_reflexive | c1:Collection(T). c1 c1 |
| def | col_union | ( i:I. C(i))(x) ==  i:I. x C(i) |
| THM | member_col_union | C:(ICollection(T)), x:T. x i:I. C(i) (i:I. x C(i)) |
| def | col_map | < f(x) | x c > (y) == x:T. x c & y = f(x) T' |
| THM | member_col_map | c:Collection(T), f:(TT'), x:T'. x < f(y) | y c > (y:T. y c & x = f(y)) |
| def | col_add | (a + b)(x) == x a  x b |
| THM | member_col_add | a,b:Collection(T), x:T. x a + b x a x b |
| def | col_accum | (xc.f(x))(y) == x:T. x c & y f(x) |
| THM | member_col_accum | c:Collection(T), f:(TCollection(T')), y:T'. y (xc.f(x)) (x:T. x c & y f(x)) |
| def | col_list_prod | col_list_prod(l)(x) == ||x|| = ||l||  & (i:. i < ||x|| x[i] l[i]) |
| THM | member_col_list_prod | l:Collection(T) List, x:T List.
x col_list_prod(l) ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i]) |
| def | col_all | (xc.P(x)) == x:T. x c P(x) |
| THM | col_all_iff | c:Collection(T), P:(TProp). (xc.P(x)) (x:T. x c P(x)) |
| THM | col_all_functionality | P:(TProp), c1,c2:Collection(T). c1 = c2 ((xc1.P(x)) (xc2.P(x))) |