meson/test/selftest.sml

2945    (!Z X. member(Z,first(X)) ==> little_set(f5(Z,X))) /\
2946    (!Z X. member(Z,first(X)) ==> equal(X,ordered_pair(f4(Z,X),f5(Z,X)))) /\
3077    (!U7 V7 W7. equal(U7,V7) ==> equal(f5(U7,W7),f5(V7,W7))) /\
3078    (!X7 Z7 Y7. equal(X7,Y7) ==> equal(f5(Z7,X7),f5(Z7,Y7))) /\
3292    (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) ==> topological_space(X,Vt) \/ element_of_collection(f3(X,Vt),Vt) \/ subset_collections(f5(X,Vt),Vt)) /\
3293    (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) /\ element_of_collection(union_of_members(f5(X,Vt)),Vt) ==> topological_space(X,Vt) \/ element_of_collection(f3(X,Vt),Vt)) /\
3294    (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) ==> topological_space(X,Vt) \/ element_of_collection(f4(X,Vt),Vt) \/ subset_collections(f5(X,Vt),Vt)) /\
3295    (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) /\ element_of_collection(union_of_members(f5(X,Vt)),Vt) ==> topological_space(X,Vt) \/ element_of_collection(f4(X,Vt),Vt)) /\
3296    (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) /\ element_of_collection(intersection_of_sets(f3(X,Vt),f4(X,Vt)),Vt) ==> topological_space(X,Vt) \/ subset_collections(f5(X,Vt),Vt)) /\
3297    (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) /\ element_of_collection(intersection_of_sets(f3(X,Vt),f4(X,Vt)),Vt) /\ element_of_collection(union_of_members(f5(X,Vt)),Vt) ==> topological_space(X,Vt)) /\