:: PRE_TOPC semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"TopStruct"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"TopStruct":::(# :::"carrier":::, :::"topology"::: #) -> ($#l1_pre_topc :::"TopStruct"::: ) ; sel :::"topology"::: "c1" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionlet "IT" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "IT" is :::"TopSpace-like"::: means :: PRE_TOPC:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT")) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT"))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT")) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT")) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT"))) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT")) ")" ) ")" ); end; :: deftheorem defines :::"TopSpace-like"::: PRE_TOPC:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT"))))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT")))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionmode TopSpace is ($#v2_pre_topc :::"TopSpace-like"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode Point of "S" is ($#m1_subset_1 :::"Element":::) "of" "S"; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: PRE_TOPC:1 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "GX"))))) ; theorem :: PRE_TOPC:2 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))))) ; theorem :: PRE_TOPC:3 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: PRE_TOPC:4 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) "iff" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: PRE_TOPC:5 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q")))) & (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P")))))) ; theorem :: PRE_TOPC:6 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" ) ($#k3_subset_1 :::"`"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "P" is :::"open"::: means :: PRE_TOPC:def 2 (Bool "P" ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T")); end; :: deftheorem defines :::"open"::: PRE_TOPC:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "P" is :::"closed"::: means :: PRE_TOPC:def 3 (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) "T" ")" ) ($#k7_subset_1 :::"\"::: ) "P") "is" ($#v3_pre_topc :::"open"::: ) ); end; :: deftheorem defines :::"closed"::: PRE_TOPC:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P"))) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; mode :::"SubSpace"::: "of" "T" -> ($#l1_pre_topc :::"TopStruct"::: ) means :: PRE_TOPC:def 4 (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "T")) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" it "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it)) "iff" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T")) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) it ")" ))) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SubSpace"::: PRE_TOPC:def 4 : (Bool "for" (Set (Var "T")) "," (Set (Var "b2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T"))) "iff" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b2")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b2")))) "iff" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b2")) ")" ))) ")" )) ")" ) ")" ) ")" ) ")" )); registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_pre_topc :::"strict"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster -> ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "T" :::"|"::: "P" -> ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "T" means :: PRE_TOPC:def 5 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) "P"); end; :: deftheorem defines :::"|"::: PRE_TOPC:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) ")" )))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "T" ($#k1_pre_topc :::"|"::: ) "P") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "T" ($#k1_pre_topc :::"|"::: ) "P") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; theorem :: PRE_TOPC:7 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P19")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P2")) ")" ) "st" (Bool (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P19"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Set (Var "S")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P2")) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P19"))))))) ; theorem :: PRE_TOPC:8 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: PRE_TOPC:9 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k5_relset_1 :::"|"::: ) (Set (Var "P"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "," (Set (Var "Y"))))))) ; definitionlet "S", "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"continuous"::: means :: PRE_TOPC:def 6 (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "P1")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "P1"))) "is" ($#v4_pre_topc :::"closed"::: ) )); end; :: deftheorem defines :::"continuous"::: PRE_TOPC:def 6 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P1")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P1"))) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))); theorem :: PRE_TOPC:10 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))) "#)" )) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S2"))) "#)" )) & (Bool (Set (Var "S1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T1")))) "holds" (Bool (Set (Var "S2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T2")))) ; theorem :: PRE_TOPC:11 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X9")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")))))) ; theorem :: PRE_TOPC:12 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "T"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_struct_0 :::"[#]"::: ) "T") -> ($#v4_pre_topc :::"closed"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: PRE_TOPC:13 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X9")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )) ")" )))) ; theorem :: PRE_TOPC:14 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); func :::"Cl"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" means :: PRE_TOPC:def 7 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "GX"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "GX" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool "A" ($#r1_xboole_0 :::"meets"::: ) (Set (Var "G")))) ")" )); projectivity (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "GX"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "b2")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "G")))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "GX"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "b1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "G")))) ")" ))) ; end; :: deftheorem defines :::"Cl"::: PRE_TOPC:def 7 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "GX"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "G")))) ")" )) ")" ))); theorem :: PRE_TOPC:15 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ")" )))) ; theorem :: PRE_TOPC:16 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool "(" (Bool "(" "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" ) ")" ) ")" ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")))) ")" )))) ; theorem :: PRE_TOPC:17 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X9")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A1")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X9")) ")" ))))))) ; theorem :: PRE_TOPC:18 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))) ; theorem :: PRE_TOPC:19 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")))))) ; theorem :: PRE_TOPC:20 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ))))) ; theorem :: PRE_TOPC:21 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ))))) ; theorem :: PRE_TOPC:22 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "implies" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" & "(" (Bool (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "implies" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ")" ))) ; theorem :: PRE_TOPC:23 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "implies" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))) ")" & "(" (Bool (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))) "implies" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ")" ))) ; theorem :: PRE_TOPC:24 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "G"))) ")" ) ")" ) ")" )))) ; begin theorem :: PRE_TOPC:25 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")))))) ; theorem :: PRE_TOPC:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "C")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "B")))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) )))) ; theorem :: PRE_TOPC:27 (Bool "for" (Set (Var "A")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "C")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "h")) "is" ($#v5_pre_topc :::"continuous"::: ) )))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "X" be ($#l1_pre_topc :::"TopSpace":::); let "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); cluster (Set "X" ($#k6_struct_0 :::"-->"::: ) "y") -> ($#v5_pre_topc :::"continuous"::: ) ; end; registrationlet "S" be ($#l1_pre_topc :::"TopSpace":::); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) bbbadV1_FUNCT_1() bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"T_0"::: means :: PRE_TOPC:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) "iff" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); attr "T" is :::"T_1"::: means :: PRE_TOPC:def 9 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k3_subset_1 :::"`"::: ) )) ")" ))); attr "T" is :::"T_2"::: means :: PRE_TOPC:def 10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G2"))) ")" ))); attr "T" is :::"regular"::: means :: PRE_TOPC:def 11 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G2"))) ")" )))); attr "T" is :::"normal"::: means :: PRE_TOPC:def 12 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "F1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "F2")))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "F1")) ($#r1_tarski :::"c="::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r1_tarski :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G2"))) ")" ))); end; :: deftheorem defines :::"T_0"::: PRE_TOPC:def 8 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) "iff" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); :: deftheorem defines :::"T_1"::: PRE_TOPC:def 9 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k3_subset_1 :::"`"::: ) )) ")" ))) ")" )); :: deftheorem defines :::"T_2"::: PRE_TOPC:def 10 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_pre_topc :::"T_2"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G2"))) ")" ))) ")" )); :: deftheorem defines :::"regular"::: PRE_TOPC:def 11 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G2"))) ")" )))) ")" )); :: deftheorem defines :::"normal"::: PRE_TOPC:def 12 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) ) "iff" (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "F2")))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "F1")) ($#r1_tarski :::"c="::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r1_tarski :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G2"))) ")" ))) ")" )); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"T_3"::: means :: PRE_TOPC:def 13 (Bool "(" (Bool "T" "is" ($#v7_pre_topc :::"T_1"::: ) ) & (Bool "T" "is" ($#v9_pre_topc :::"regular"::: ) ) ")" ); attr "T" is :::"T_4"::: means :: PRE_TOPC:def 14 (Bool "(" (Bool "T" "is" ($#v7_pre_topc :::"T_1"::: ) ) & (Bool "T" "is" ($#v10_pre_topc :::"normal"::: ) ) ")" ); end; :: deftheorem defines :::"T_3"::: PRE_TOPC:def 13 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v11_pre_topc :::"T_3"::: ) ) "iff" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) & (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) ")" ) ")" )); :: deftheorem defines :::"T_4"::: PRE_TOPC:def 14 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v12_pre_topc :::"T_4"::: ) ) "iff" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) & (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) ) ")" ) ")" )); registration cluster ($#v11_pre_topc :::"T_3"::: ) -> ($#v7_pre_topc :::"T_1"::: ) ($#v9_pre_topc :::"regular"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v7_pre_topc :::"T_1"::: ) ($#v9_pre_topc :::"regular"::: ) -> ($#v11_pre_topc :::"T_3"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v12_pre_topc :::"T_4"::: ) -> ($#v7_pre_topc :::"T_1"::: ) ($#v10_pre_topc :::"normal"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v7_pre_topc :::"T_1"::: ) ($#v10_pre_topc :::"normal"::: ) -> ($#v12_pre_topc :::"T_4"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v7_pre_topc :::"T_1"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#v7_pre_topc :::"T_1"::: ) -> ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v8_pre_topc :::"T_2"::: ) -> ($#v7_pre_topc :::"T_1"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T") "#)" ) -> ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T") "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: PRE_TOPC:28 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) )) ; theorem :: PRE_TOPC:29 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) "holds" (Bool (Set (Var "S")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T"))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: PRE_TOPC:30 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) ")" ))) ; theorem :: PRE_TOPC:31 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "X")) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) ")" ))) ; theorem :: PRE_TOPC:32 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ; theorem :: PRE_TOPC:33 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ; theorem :: PRE_TOPC:34 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) "," (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )))) ; registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "T" ($#k1_pre_topc :::"|"::: ) "P") -> ($#v2_struct_0 :::"empty"::: ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: PRE_TOPC:35 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "S")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) ")" )) ; theorem :: PRE_TOPC:36 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "X")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "X")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "Y"))))))) ; registration cluster ($#v2_struct_0 :::"empty"::: ) ($#v1_pre_topc :::"strict"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "A")); cluster (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" "A" "," "t" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#v2_struct_0 :::"empty"::: ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end;