:: TOPGEN_1 semantic presentation begin theorem :: TOPGEN_1:1 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )) "iff" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: TOPGEN_1:2 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_orders_4 :::"countable"::: ) ) "iff" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )) ; registrationlet "T" be ($#v8_struct_0 :::"finite"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "T") -> ($#v1_finset_1 :::"finite"::: ) ; end; registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v1_orders_4 :::"countable"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_4 :::"countable"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_orders_4 :::"countable"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "T" be ($#v1_orders_4 :::"countable"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "T") -> ($#v4_card_3 :::"countable"::: ) ; 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; begin theorem :: TOPGEN_1:3 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); func :::"Fr"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" means :: TOPGEN_1:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "F") ")" )) ")" )); end; :: deftheorem defines :::"Fr"::: TOPGEN_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" )) ")" ))); theorem :: TOPGEN_1:4 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPGEN_1:5 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: TOPGEN_1:6 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "G")))))) ; theorem :: TOPGEN_1:7 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_topgen_1 :::"Fr"::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "F")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_topgen_1 :::"Fr"::: ) (Set (Var "G")) ")" ))))) ; theorem :: TOPGEN_1:8 (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 ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))))) ; theorem :: TOPGEN_1:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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_tops_1 :::"Fr"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "U")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "U"))) & (Bool (Set (Set (Var "U")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ")" )))) ; theorem :: TOPGEN_1:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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_tops_1 :::"Fr"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "U"))) & (Bool (Set (Set (Var "U")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ")" )))) ; theorem :: TOPGEN_1:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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_tops_1 :::"Fr"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" "st" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "U"))) & (Bool (Set (Set (Var "U")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ")" )))) ; theorem :: TOPGEN_1:12 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "B")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: TOPGEN_1:13 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: TOPGEN_1:14 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (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"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) "iff" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "x" be ($#m1_hidden :::"set"::: ) ; pred "x" :::"is_an_accumulation_point_of"::: "A" means :: TOPGEN_1:def 2 (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" "A" ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ))); end; :: deftheorem defines :::"is_an_accumulation_point_of"::: TOPGEN_1:def 2 : (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 "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" )))); theorem :: TOPGEN_1:15 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")))))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Der"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "T" means :: TOPGEN_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) "A") ")" )); end; :: deftheorem defines :::"Der"::: TOPGEN_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A"))) ")" )) ")" ))); theorem :: TOPGEN_1:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A"))) ")" )))) ; theorem :: TOPGEN_1:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "U")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "U")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" ))) ")" )))) ; theorem :: TOPGEN_1:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "U")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" )))) ")" )))) ; theorem :: TOPGEN_1:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" "st" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "U")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" )))) ")" )))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "x" be ($#m1_hidden :::"set"::: ) ; pred "x" :::"is_isolated_in"::: "A" means :: TOPGEN_1:def 4 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) "A") & (Bool (Bool "not" "x" ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) "A")) ")" ); end; :: deftheorem defines :::"is_isolated_in"::: TOPGEN_1:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_topgen_1 :::"is_isolated_in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A")))) ")" ) ")" )))); theorem :: TOPGEN_1:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")) ")" ))) "iff" (Bool (Set (Var "p")) ($#r2_topgen_1 :::"is_isolated_in"::: ) (Set (Var "A"))) ")" )))) ; theorem :: TOPGEN_1:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "U")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) ")" ))) ")" )))) ; theorem :: TOPGEN_1:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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_topgen_1 :::"is_isolated_in"::: ) (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "G")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Set (Set (Var "G")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))) ")" )))) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); attr "p" is :::"isolated"::: means :: TOPGEN_1:def 5 (Bool "p" ($#r2_topgen_1 :::"is_isolated_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "T")); end; :: deftheorem defines :::"isolated"::: TOPGEN_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_topgen_1 :::"isolated"::: ) ) "iff" (Bool (Set (Var "p")) ($#r2_topgen_1 :::"is_isolated_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) ")" ))); theorem :: TOPGEN_1:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_topgen_1 :::"isolated"::: ) ) "iff" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); func :::"Der"::: "F" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" means :: TOPGEN_1:def 6 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "F") ")" )) ")" )); end; :: deftheorem defines :::"Der"::: TOPGEN_1:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" )) ")" ))); theorem :: TOPGEN_1:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPGEN_1:25 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: TOPGEN_1:26 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topgen_1 :::"Der"::: ) (Set (Var "G")))))) ; theorem :: TOPGEN_1:27 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_topgen_1 :::"Der"::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topgen_1 :::"Der"::: ) (Set (Var "G")) ")" ))))) ; theorem :: TOPGEN_1:28 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))) ; theorem :: TOPGEN_1:29 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")) ")" ))))) ; theorem :: TOPGEN_1:30 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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_topgen_1 :::"Der"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "B")))))) ; theorem :: TOPGEN_1:31 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "B")) ")" ))))) ; theorem :: TOPGEN_1:32 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) "holds" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))))) ; theorem :: TOPGEN_1:33 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_pre_topc :::"T_1"::: ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_topgen_1 :::"Der"::: ) "A") -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: TOPGEN_1:34 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ))))) ; theorem :: TOPGEN_1:35 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r1_topgen_1 :::"is_an_accumulation_point_of"::: ) (Set (Var "B")))))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "A" is :::"dense-in-itself"::: means :: TOPGEN_1:def 7 (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) "A")); end; :: deftheorem defines :::"dense-in-itself"::: TOPGEN_1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A")))) ")" ))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "T" is :::"dense-in-itself"::: means :: TOPGEN_1:def 8 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "T") "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ); end; :: deftheorem defines :::"dense-in-itself"::: TOPGEN_1:def 8 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v3_topgen_1 :::"dense-in-itself"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) ")" )); theorem :: TOPGEN_1:36 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is :::"dense-in-itself"::: means :: TOPGEN_1:def 9 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "A")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) )); end; :: deftheorem defines :::"dense-in-itself"::: TOPGEN_1:def 9 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_topgen_1 :::"dense-in-itself"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "A")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) )) ")" ))); theorem :: TOPGEN_1:37 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_topgen_1 :::"dense-in-itself"::: ) )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k3_topgen_1 :::"Der"::: ) (Set (Var "F")) ")" ))))) ; theorem :: TOPGEN_1:38 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_topgen_1 :::"dense-in-itself"::: ) )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ))) ; theorem :: TOPGEN_1:39 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v3_pre_topc "non" ($#v3_pre_topc :::"open"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); cluster ($#~v4_pre_topc "non" ($#v4_pre_topc :::"closed"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v3_pre_topc "non" ($#v3_pre_topc :::"open"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v4_pre_topc "non" ($#v4_pre_topc :::"closed"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "A" is :::"perfect"::: means :: TOPGEN_1:def 10 (Bool "(" (Bool "A" "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "A" "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) ")" ); end; :: deftheorem defines :::"perfect"::: TOPGEN_1:def 10 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_topgen_1 :::"perfect"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) ")" ) ")" ))); registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v5_topgen_1 :::"perfect"::: ) -> ($#v4_pre_topc :::"closed"::: ) ($#v2_topgen_1 :::"dense-in-itself"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); cluster ($#v4_pre_topc :::"closed"::: ) ($#v2_topgen_1 :::"dense-in-itself"::: ) -> ($#v5_topgen_1 :::"perfect"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; theorem :: TOPGEN_1:40 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "T"))))) ; theorem :: TOPGEN_1:41 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_topgen_1 :::"perfect"::: ) ) "iff" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))) ; theorem :: TOPGEN_1:42 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "T"))) "is" ($#v5_topgen_1 :::"perfect"::: ) )) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v5_topgen_1 :::"perfect"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v5_topgen_1 :::"perfect"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "A" is :::"scattered"::: means :: TOPGEN_1:def 11 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) "A") "or" "not" (Bool (Set (Var "B")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) ")" )); end; :: deftheorem defines :::"scattered"::: TOPGEN_1:def 11 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_topgen_1 :::"scattered"::: ) ) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" "not" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" "not" (Bool (Set (Var "B")) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) ")" )) ")" ))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_topgen_1 :::"scattered"::: ) -> ($#~v2_topgen_1 "non" ($#v2_topgen_1 :::"dense-in-itself"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_topgen_1 :::"dense-in-itself"::: ) -> ($#~v6_topgen_1 "non" ($#v6_topgen_1 :::"scattered"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; theorem :: TOPGEN_1:43 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "T"))) "is" ($#v6_topgen_1 :::"scattered"::: ) )) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v6_topgen_1 :::"scattered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; theorem :: TOPGEN_1:44 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) "holds" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v5_topgen_1 :::"perfect"::: ) ) & (Bool (Set (Var "B")) "is" ($#v6_topgen_1 :::"scattered"::: ) ) ")" ))) ; registrationlet "T" be ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "T" be ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster -> ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; theorem :: TOPGEN_1:45 (Bool "for" (Set (Var "T")) "being" ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_topgen_1 :::"Der"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); func :::"density"::: "T" -> ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) means :: TOPGEN_1:def 12 (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A")))) ")" )) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool it ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B")))) ")" ) ")" ); end; :: deftheorem defines :::"density"::: TOPGEN_1:def 12 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_topgen_1 :::"density"::: ) (Set (Var "T")))) "iff" (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A")))) ")" )) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Var "b2")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B")))) ")" ) ")" ) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); attr "T" is :::"separable"::: means :: TOPGEN_1:def 13 (Bool (Set ($#k4_topgen_1 :::"density"::: ) "T") ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )); end; :: deftheorem defines :::"separable"::: TOPGEN_1:def 13 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_topgen_1 :::"separable"::: ) ) "iff" (Bool (Set ($#k4_topgen_1 :::"density"::: ) (Set (Var "T"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )); theorem :: TOPGEN_1:46 (Bool "for" (Set (Var "T")) "being" ($#v1_orders_4 :::"countable"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Var "T")) "is" ($#v7_topgen_1 :::"separable"::: ) )) ; registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_orders_4 :::"countable"::: ) -> ($#v7_topgen_1 :::"separable"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; begin theorem :: TOPGEN_1:47 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ))) ; theorem :: TOPGEN_1:48 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) ; theorem :: TOPGEN_1:49 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: TOPGEN_1:50 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: TOPGEN_1:51 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: TOPGEN_1:52 (Bool (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: TOPGEN_1:53 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) "is" ($#v2_tops_1 :::"boundary"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: TOPGEN_1:54 (Bool (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ) "is" ($#v2_tops_1 :::"boundary"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: TOPGEN_1:55 (Bool (Set ($#k1_numbers :::"REAL"::: ) ) "is" ($#~v2_tops_1 "non" ($#v2_tops_1 :::"boundary"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: TOPGEN_1:56 (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v2_tops_1 :::"boundary"::: ) )) ")" )) ;