:: TOPGEN_2 semantic presentation begin theorem :: TOPGEN_2:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "{" (Set (Var "U")) where U "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")))))) ; theorem :: TOPGEN_2:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x"))) ")" )) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "B"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); func :::"Chi"::: "(" "x" "," "T" ")" -> ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) means :: TOPGEN_2:def 1 (Bool "(" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" "x" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B"))))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" "x" "holds" (Bool it ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B")))) ")" ) ")" ); end; :: deftheorem defines :::"Chi"::: TOPGEN_2:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b3")) "being" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," (Set (Var "T")) ")" )) "iff" (Bool "(" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B"))))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "holds" (Bool (Set (Var "b3")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B")))) ")" ) ")" ) ")" )))); theorem :: TOPGEN_2:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) "is" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) "is" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) )) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; func :::"Chi"::: "T" -> ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) means :: TOPGEN_2:def 2 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "holds" (Bool (Set ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," "T" ")" ) ($#r1_ordinal1 :::"c="::: ) it) ")" ) & (Bool "(" "for" (Set (Var "M")) "being" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "holds" (Bool (Set ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," "T" ")" ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "M"))) ")" )) "holds" (Bool it ($#r1_ordinal1 :::"c="::: ) (Set (Var "M"))) ")" ) ")" ); end; :: deftheorem defines :::"Chi"::: TOPGEN_2:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_2 :::"Chi"::: ) (Set (Var "T")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," (Set (Var "T")) ")" ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b2"))) ")" ) & (Bool "(" "for" (Set (Var "M")) "being" ($#v1_card_1 :::"cardinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," (Set (Var "T")) ")" ) ($#r1_ordinal1 :::"c="::: ) (Set (Var "M"))) ")" )) "holds" (Bool (Set (Var "b2")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "M"))) ")" ) ")" ) ")" ))); theorem :: TOPGEN_2:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k2_topgen_2 :::"Chi"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," (Set (Var "T")) ")" ")" ) where x "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) : (Bool verum) "}" ))) ; theorem :: TOPGEN_2:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_topgen_2 :::"Chi"::: ) "(" (Set (Var "x")) "," (Set (Var "T")) ")" ) ($#r1_ordinal1 :::"c="::: ) (Set ($#k2_topgen_2 :::"Chi"::: ) (Set (Var "T")))))) ; theorem :: TOPGEN_2:6 (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" ($#v1_frechet :::"first-countable"::: ) ) "iff" (Bool (Set ($#k2_topgen_2 :::"Chi"::: ) (Set (Var "T"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); mode :::"Neighborhood_System"::: "of" "T" -> ($#m1_hidden :::"ManySortedSet":::) "of" "T" means :: TOPGEN_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")))); end; :: deftheorem defines :::"Neighborhood_System"::: TOPGEN_2:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_topgen_2 :::"Neighborhood_System"::: ) "of" (Set (Var "T"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")))) ")" ))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "N" be ($#m1_topgen_2 :::"Neighborhood_System"::: ) "of" (Set (Const "T")); :: original: :::"Union"::: redefine func :::"Union"::: "N" -> ($#m1_subset_1 :::"Basis":::) "of" "T"; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); :: original: :::"."::: redefine func "N" :::"."::: "x" -> ($#m1_subset_1 :::"Basis":::) "of" "x"; end; theorem :: TOPGEN_2:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "y")) (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B2")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) ")" ))))))) ; theorem :: TOPGEN_2:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "U1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "U2")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "U1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "U2")))) ")" )))))) ; theorem :: TOPGEN_2: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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "U")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))))) ")" )))) ; theorem :: TOPGEN_2: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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool "for" (Set (Var "U")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "U")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))))) ")" )))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_tops_2 :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); end; begin theorem :: TOPGEN_2:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#v1_tops_2 :::"open"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "G")) "being" ($#v1_tops_2 :::"open"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "S")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "G"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T")))) ")" )))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"finite-weight"::: means :: TOPGEN_2:def 4 (Bool (Set ($#k2_waybel23 :::"weight"::: ) "T") "is" ($#v1_finset_1 :::"finite"::: ) ); end; :: deftheorem defines :::"finite-weight"::: TOPGEN_2:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_topgen_2 :::"finite-weight"::: ) ) "iff" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )); notationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; antonym :::"infinite-weight"::: "T" for :::"finite-weight"::: ; end; registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v1_topgen_2 :::"finite-weight"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_topgen_2 :::"infinite-weight"::: ) -> ($#v8_struct_0 :::"infinite"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TOPGEN_2:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) ; theorem :: TOPGEN_2:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ) ")" )) ; theorem :: TOPGEN_2:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))))) ; registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_topgen_2 :::"infinite-weight"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TOPGEN_2:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topgen_2 :::"finite-weight"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "ex" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (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 "B0")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (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 (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) ")" ) ")" ) ")" ) ")" )))) ; theorem :: TOPGEN_2:16 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B0")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (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 "B0")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (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 (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "B0")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))))) ; theorem :: TOPGEN_2:17 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (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 "B0")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (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 (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "U"))) ")" ) ")" ) ")" )) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B0"))))))) ; theorem :: TOPGEN_2:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel23 :::"weight"::: ) (Set (Var "T")))) ")" )))) ; begin definitionlet "X", "x0" be ($#m1_hidden :::"set"::: ) ; func :::"DiscrWithInfin"::: "(" "X" "," "x0" ")" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) means :: TOPGEN_2:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "X") & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "U")) where U "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Bool "not" "x0" ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ")" ) where F "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" )) ")" ); end; :: deftheorem defines :::"DiscrWithInfin"::: TOPGEN_2:def 5 : (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "U")) where U "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Bool "not" (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ")" ) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" )) ")" ) ")" ))); registrationlet "X", "x0" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" "X" "," "x0" ")" ) -> ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x0" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" "X" "," "x0" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: TOPGEN_2:19 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" "not" (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" ))) ; theorem :: TOPGEN_2:20 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "not" (Bool "(" (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Bool "not" (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )) ")" ))) ; theorem :: TOPGEN_2:21 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ))) ; theorem :: TOPGEN_2:22 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "x0")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ))) ; theorem :: TOPGEN_2:23 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "U")) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: TOPGEN_2:24 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: TOPGEN_2: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")) "st" (Bool (Bool (Bool "not" (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: TOPGEN_2:26 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: TOPGEN_2:27 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: TOPGEN_2:28 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: TOPGEN_2:29 (Bool "for" (Set (Var "X")) "," (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ")" ) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" )))) ; theorem :: TOPGEN_2:30 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) ; theorem :: TOPGEN_2:31 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set "(" (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ")" ) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) ; theorem :: TOPGEN_2:32 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "F")) ($#k3_subset_1 :::"`"::: ) ")" ) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" ))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))))) ; theorem :: TOPGEN_2:33 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B"))))))) ; theorem :: TOPGEN_2:34 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_waybel23 :::"weight"::: ) (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X")))))) ; theorem :: TOPGEN_2:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x0")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "B0")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set "(" ($#k5_topgen_2 :::"DiscrWithInfin"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool verum) "}" ))))) ; begin theorem :: TOPGEN_2:36 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "F")) "st" (Bool (Bool "(" "for" (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_subset_1 :::"\"::: ) (Set (Var "G"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "G")) ")" ) ")" ) where G "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) : (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "}" ")" )))))) ; theorem :: TOPGEN_2:37 (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 (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_pcomps_1 :::"clf"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "G")) ")" ) ")" ) where G "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "F")) ($#k7_subset_1 :::"\"::: ) (Set (Var "G"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) "}" ")" ))))) ; theorem :: TOPGEN_2:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "o")) "#)" ) "is" ($#l1_pre_topc :::"TopSpace":::)) ")" )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "O")))) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "B")) "#)" ) "is" ($#l1_pre_topc :::"TopSpace":::)) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "o")) "#)" ) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "B")) "#)" )) ")" ) & (Bool "(" "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "o")) "#)" ) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T"))) ")" )) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "B")) "#)" ) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T"))) ")" ) ")" )))) ; theorem :: TOPGEN_2:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set "(" ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "O")) ")" ) ")" ))) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "B")) "#)" ) "is" ($#l1_pre_topc :::"TopSpace":::)) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "B")) "#)" ) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "o")) "#)" )) ")" ) & (Bool "(" "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "o")) "#)" )) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set (Var "X")) "," (Set (Var "B")) "#)" )) ")" ) ")" )))) ;