:: YELLOW_8 semantic presentation begin theorem :: YELLOW_8:1 (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))))) ; theorem :: YELLOW_8:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")))))) ; begin theorem :: YELLOW_8:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "F")) "," (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r2_tarski :::"are_equipotent"::: ) ))) ; theorem :: YELLOW_8:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r2_tarski :::"are_equipotent"::: ) ) & (Bool (Set (Var "X")) "is" ($#v4_card_3 :::"countable"::: ) )) "holds" (Bool (Set (Var "Y")) "is" ($#v4_card_3 :::"countable"::: ) )) ; theorem :: YELLOW_8:5 (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )))) ; theorem :: YELLOW_8:6 (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: YELLOW_8:7 (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; begin theorem :: YELLOW_8:8 (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 "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")))))) ; theorem :: YELLOW_8:9 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ) "}" ))))) ; theorem :: YELLOW_8:10 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: YELLOW_8:11 (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 "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" ) "}" ))))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is "x" :::"-quasi_basis"::: means :: YELLOW_8:def 1 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) "F")) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"-quasi_basis"::: YELLOW_8: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 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Var "x")) ($#v1_yellow_8 :::"-quasi_basis"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) ")" )) ")" ) ")" ) ")" )))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster ($#v1_tops_2 :::"open"::: ) "x" ($#v1_yellow_8 :::"-quasi_basis"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); mode Basis of "x" is ($#v1_tops_2 :::"open"::: ) "x" ($#v1_yellow_8 :::"-quasi_basis"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" "T"; end; theorem :: YELLOW_8:12 (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")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ))))) ; theorem :: YELLOW_8:13 (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")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "W")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "W")) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )))))) ; theorem :: YELLOW_8:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x")) "st" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) ")" )) "holds" (Bool (Set (Var "P")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "T" is :::"Baire"::: means :: YELLOW_8:def 2 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) ) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "S")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "I")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))); end; :: deftheorem defines :::"Baire"::: YELLOW_8:def 2 : (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" ($#v2_yellow_8 :::"Baire"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) ) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "S")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "F")))) & (Bool (Set (Var "I")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))) ")" )); theorem :: YELLOW_8:15 (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" ($#v2_yellow_8 :::"Baire"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) ) & (Bool "(" "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "S")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) ")" )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v2_tops_1 :::"boundary"::: ) )) ")" )) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "S" is :::"irreducible"::: means :: YELLOW_8:def 3 (Bool "(" (Bool (Bool "not" "S" "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "S" "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "(" "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "S1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "S2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "S" ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "S2")))) & (Bool (Bool "not" (Set (Var "S1")) ($#r1_hidden :::"="::: ) "S"))) "holds" (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) "S") ")" ) ")" ); end; :: deftheorem defines :::"irreducible"::: YELLOW_8:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_yellow_8 :::"irreducible"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "S")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "S")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "(" "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "S2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "S2")))) & (Bool (Bool "not" (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set (Var "S"))) ")" ) ")" ) ")" ))); registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v3_yellow_8 :::"irreducible"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); pred "p" :::"is_dense_point_of"::: "S" means :: YELLOW_8:def 4 (Bool "(" (Bool "p" ($#r2_hidden :::"in"::: ) "S") & (Bool "S" ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) "p" ($#k6_domain_1 :::"}"::: ) ))) ")" ); end; :: deftheorem defines :::"is_dense_point_of"::: YELLOW_8:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "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_yellow_8 :::"is_dense_point_of"::: ) (Set (Var "S"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))) ")" ) ")" )))); theorem :: YELLOW_8:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: YELLOW_8:17 (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 (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v3_yellow_8 :::"irreducible"::: ) ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_yellow_8 :::"irreducible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "T" is :::"sober"::: means :: YELLOW_8:def 5 (Bool "for" (Set (Var "S")) "being" ($#v3_yellow_8 :::"irreducible"::: ) ($#m1_subset_1 :::"Subset":::) "of" "T" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool (Bool (Set (Var "q")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ) ")" ))); end; :: deftheorem defines :::"sober"::: YELLOW_8:def 5 : (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" ($#v4_yellow_8 :::"sober"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v3_yellow_8 :::"irreducible"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "q")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ) ")" ))) ")" )); theorem :: YELLOW_8:18 (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 (Set (Var "p")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: YELLOW_8:19 (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 (Set (Var "p")) ($#r1_yellow_8 :::"is_dense_point_of"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: YELLOW_8:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k2_finsub_1 :::"\"::: ) (Set (Var "G"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: YELLOW_8:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#v3_yellow_8 :::"irreducible"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "S")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_yellow_8 :::"irreducible"::: ) -> ($#v1_zfmisc_1 :::"trivial"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: YELLOW_8:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Var "T")) "is" ($#v4_yellow_8 :::"sober"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"Hausdorff"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_8 :::"sober"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_yellow_8 :::"sober"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: YELLOW_8:23 (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" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ")" )) ; theorem :: YELLOW_8:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_8 :::"sober"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Var "T")) "is" ($#v6_pre_topc :::"T_0"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_yellow_8 :::"sober"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"CofinTop"::: "X" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) means :: YELLOW_8:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "X") & (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it)) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) "X" ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "X" ")" ))) ")" ); end; :: deftheorem defines :::"CofinTop"::: YELLOW_8:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_8 :::"CofinTop"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b2")))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")) ")" ))) ")" ) ")" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_yellow_8 :::"CofinTop"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_yellow_8 :::"CofinTop"::: ) "X") -> ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; theorem :: YELLOW_8:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_yellow_8 :::"CofinTop"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) "or" (Bool (Set (Var "P")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" ))) ; theorem :: YELLOW_8:26 (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 "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_yellow_8 :::"CofinTop"::: ) "X") -> ($#v1_pre_topc :::"strict"::: ) ($#v7_pre_topc :::"T_1"::: ) ; end; registrationlet "X" be ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_yellow_8 :::"CofinTop"::: ) "X") -> ($#v1_pre_topc :::"strict"::: ) ($#~v4_yellow_8 "non" ($#v4_yellow_8 :::"sober"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v7_pre_topc :::"T_1"::: ) ($#~v4_yellow_8 "non" ($#v4_yellow_8 :::"sober"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; begin theorem :: YELLOW_8:27 (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" ($#v9_pre_topc :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "Q")))) ")" )))) ")" )) ; theorem :: YELLOW_8:28 (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" ($#v9_pre_topc :::"regular"::: ) )) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v6_waybel_3 :::"locally-compact"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "Y")))) & (Bool (Set (Var "Y")) "is" ($#v2_compts_1 :::"compact"::: ) ) ")" ))) ")" )) ;