:: TEX_4 semantic presentation begin registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "A") -> ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ; end; registrationlet "X" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "A") -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; theorem :: TEX_4:1 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) "}" )))) ; theorem :: TEX_4:2 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k1_tops_1 :::"Int"::: ) "A") -> ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k1_tops_1 :::"Int"::: ) "A") -> ($#v1_subset_1 :::"proper"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set ($#k1_tops_1 :::"Int"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: TEX_4:3 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) "}" )))) ; begin definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); attr "IT" is :::"anti-discrete"::: means :: TEX_4:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Var "G"))))); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 1 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ")" ))); definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); redefine attr "A" is :::"anti-discrete"::: means :: TEX_4:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "F"))))); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 2 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))))) ")" ))); definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); redefine attr "A" is :::"anti-discrete"::: means :: TEX_4:def 3 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool "A" ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G"))) "or" (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "G"))) ")" )); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 3 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) ")" )) ")" ))); definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); redefine attr "A" is :::"anti-discrete"::: means :: TEX_4:def 4 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" (Bool "A" ($#r1_xboole_0 :::"misses"::: ) (Set (Var "F"))) "or" (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" )); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 4 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "F"))) "or" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" )) ")" ))); theorem :: TEX_4:4 (Bool "for" (Set (Var "Y0")) "," (Set (Var "Y1")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "D0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y1")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y0"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" )) & (Bool (Set (Var "D0")) ($#r1_hidden :::"="::: ) (Set (Var "D1"))) & (Bool (Set (Var "D0")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )) "holds" (Bool (Set (Var "D1")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )))) ; theorem :: TEX_4:5 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ))) ; theorem :: TEX_4:6 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ))) ; theorem :: TEX_4:7 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ))) ; definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Y")); attr "IT" is :::"anti-discrete-set-family"::: means :: TEX_4:def 5 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )); end; :: deftheorem defines :::"anti-discrete-set-family"::: TEX_4:def 5 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_tex_4 :::"anti-discrete-set-family"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )) ")" ))); theorem :: TEX_4:8 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tex_4 :::"anti-discrete-set-family"::: ) ) & (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ))) ; theorem :: TEX_4:9 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tex_4 :::"anti-discrete-set-family"::: ) )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ))) ; definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); func :::"MaxADSF"::: "x" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "Y" equals :: TEX_4:def 6 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "Y" : (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" ; end; :: deftheorem defines :::"MaxADSF"::: TEX_4:def 6 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_tex_4 :::"MaxADSF"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) "}" ))); registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); cluster (Set ($#k1_tex_4 :::"MaxADSF"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TEX_4:10 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k1_tex_4 :::"MaxADSF"::: ) (Set (Var "x"))) "is" ($#v2_tex_4 :::"anti-discrete-set-family"::: ) ))) ; theorem :: TEX_4:11 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k1_tex_4 :::"MaxADSF"::: ) (Set (Var "x")) ")" ))))) ; theorem :: TEX_4:12 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_tex_4 :::"MaxADSF"::: ) (Set (Var "x")) ")" ))))) ; theorem :: TEX_4:13 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_tex_4 :::"MaxADSF"::: ) (Set (Var "x")) ")" )) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ))) ; begin definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); attr "IT" is :::"maximal_anti-discrete"::: means :: TEX_4:def 7 (Bool "(" (Bool "IT" "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"maximal_anti-discrete"::: TEX_4:def 7 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))); theorem :: TEX_4:14 (Bool "for" (Set (Var "Y0")) "," (Set (Var "Y1")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "D0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y1")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y0"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" )) & (Bool (Set (Var "D0")) ($#r1_hidden :::"="::: ) (Set (Var "D1"))) & (Bool (Set (Var "D0")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) )) "holds" (Bool (Set (Var "D1")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) )))) ; theorem :: TEX_4:15 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Bool "not" (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) )))) ; theorem :: TEX_4:16 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ))) ; theorem :: TEX_4:17 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ))) ; definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); func :::"MaxADSet"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "Y" equals :: TEX_4:def 8 (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_tex_4 :::"MaxADSF"::: ) "x" ")" )); end; :: deftheorem defines :::"MaxADSet"::: TEX_4:def 8 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k1_tex_4 :::"MaxADSF"::: ) (Set (Var "x")) ")" ))))); registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); cluster (Set ($#k2_tex_4 :::"MaxADSet"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TEX_4:18 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))))) ; theorem :: TEX_4:19 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))))))) ; theorem :: TEX_4:20 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ))) ; theorem :: TEX_4:21 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) "iff" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) ")" ))) ; theorem :: TEX_4:22 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) "or" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) ")" ))) ; theorem :: TEX_4:23 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "F")))))) ; theorem :: TEX_4:24 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "G")))))) ; theorem :: TEX_4:25 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" )))) ; theorem :: TEX_4:26 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )))) ; definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); redefine attr "A" is :::"maximal_anti-discrete"::: means :: TEX_4:def 9 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) ")" )); end; :: deftheorem defines :::"maximal_anti-discrete"::: TEX_4:def 9 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) ")" )) ")" ))); theorem :: TEX_4:27 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))))))) ; definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); redefine attr "A" is :::"maximal_anti-discrete"::: means :: TEX_4:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "A" ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"maximal_anti-discrete"::: TEX_4:def 10 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))))) ")" ))); definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); func :::"MaxADSet"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "Y" equals :: TEX_4:def 11 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Point":::) "of" "Y" : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") "}" ); end; :: deftheorem defines :::"MaxADSet"::: TEX_4:def 11 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" )))); theorem :: TEX_4:28 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: TEX_4:29 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:30 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))))))) ; theorem :: TEX_4:31 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B")))))) ; theorem :: TEX_4:32 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:33 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" ))))) ; theorem :: TEX_4:34 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B")))))) ; theorem :: TEX_4:35 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B")))))) ; theorem :: TEX_4:36 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B")) ")" ))))) ; theorem :: TEX_4:37 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B")) ")" ))))) ; registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k3_tex_4 :::"MaxADSet"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k3_tex_4 :::"MaxADSet"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k3_tex_4 :::"MaxADSet"::: ) "A") -> ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ; end; registrationlet "Y" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k3_tex_4 :::"MaxADSet"::: ) "A") -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; theorem :: TEX_4:38 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ; theorem :: TEX_4:39 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) ")" ) "}" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) ")" ) "}" )))) ; theorem :: TEX_4:40 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "F"))))) ; theorem :: TEX_4:41 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) "}" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) "}" )))) ; begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"anti-discrete"::: means :: TEX_4:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 12 : (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"anti-discrete"::: means :: TEX_4:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) "A") ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 13 : (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"anti-discrete"::: means :: TEX_4:def 14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"anti-discrete"::: TEX_4:def 14 : (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) ")" ))); theorem :: TEX_4:42 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: TEX_4:43 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ")" ))) ; theorem :: TEX_4:44 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Bool "not" (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ))) ; theorem :: TEX_4:45 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ))) ; theorem :: TEX_4:46 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )))) ; theorem :: TEX_4:47 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) "}" )))) ; theorem :: TEX_4:48 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: TEX_4:49 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: TEX_4:50 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); :: original: :::"MaxADSet"::: redefine func :::"MaxADSet"::: "x" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: TEX_4:def 15 (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" ")" )); end; :: deftheorem defines :::"MaxADSet"::: TEX_4:def 15 : (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" ")" ))))); theorem :: TEX_4:51 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )) ")" ))) ; theorem :: TEX_4:52 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) ")" ) "}" )) ")" ))) ; theorem :: TEX_4:53 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) "iff" (Bool "(" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) ")" )) "or" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "W")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) & (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set (Var "W"))) ")" )) ")" ) ")" ))) ; theorem :: TEX_4:54 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool "(" (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) "iff" (Bool "(" (Bool "ex" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) & (Bool (Set (Var "E")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y")))) ")" )) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) & (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" )) ")" ) ")" ))) ; theorem :: TEX_4:55 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) ")" ) "}" )))) ; theorem :: TEX_4:56 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: TEX_4:57 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:58 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) "}" )))) ; theorem :: TEX_4:59 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:60 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: TEX_4:61 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:62 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:63 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")))))) ; theorem :: TEX_4:64 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "P")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "Q")) ")" ))))) ; theorem :: TEX_4:65 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) "holds" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "P")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "Q")) ")" ))))) ; begin theorem :: TEX_4:66 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0")))) & (Bool (Set (Var "Y0")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )))) ; theorem :: TEX_4:67 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y0")) "is" ($#v2_pre_topc :::"TopSpace-like"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0")))) & (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) )) "holds" (Bool (Set (Var "Y0")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) )))) ; theorem :: TEX_4:68 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "X0")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "Y0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) ")" ) ")" )) "holds" (Bool (Set (Var "Y0")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ))) ; theorem :: TEX_4:69 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "X0")) "being" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "Y0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) ")" ) ")" )) "holds" (Bool (Set (Var "Y0")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ))) ; theorem :: TEX_4:70 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X0")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "Y0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) ")" )))) ; theorem :: TEX_4:71 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X0")) "being" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "Y0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) ")" )))) ; definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "Y")); attr "IT" is :::"maximal_anti-discrete"::: means :: TEX_4:def 16 (Bool "(" (Bool "IT" "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) & (Bool "(" "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y" "st" (Bool (Bool (Set (Var "Y0")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0")))) ")" ) ")" ); end; :: deftheorem defines :::"maximal_anti-discrete"::: TEX_4:def 16 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) & (Bool "(" "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y0")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0")))) ")" ) ")" ) ")" ))); registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v4_tex_4 :::"maximal_anti-discrete"::: ) -> ($#v2_tdlat_3 :::"anti-discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y"; cluster ($#~v2_tdlat_3 "non" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) -> ($#~v4_tex_4 "non" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y"; end; theorem :: TEX_4:72 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))) "holds" (Bool "(" (Bool (Set (Var "Y0")) "is" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tex_4 :::"maximal_anti-discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#~v4_tex_4 "non" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v2_tdlat_3 "non" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#~v4_tex_4 "non" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tsep_1 "non" ($#v1_tsep_1 :::"open"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tex_4 :::"maximal_anti-discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#~v4_tex_4 "non" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v2_tdlat_3 "non" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#~v4_tex_4 "non" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_borsuk_1 "non" ($#v1_borsuk_1 :::"closed"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); func :::"MaxADSspace"::: "x" -> ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y" means :: TEX_4:def 17 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) "x")); end; :: deftheorem defines :::"MaxADSspace"::: TEX_4:def 17 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tex_4 :::"MaxADSet"::: ) (Set (Var "x")))) ")" )))); registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "Y")); cluster (Set ($#k5_tex_4 :::"MaxADSspace"::: ) "x") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: TEX_4:73 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#k1_tex_2 :::"Sspace"::: ) (Set (Var "x"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")))))) ; theorem :: TEX_4:74 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "iff" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "y")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "y")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "#)" )) ")" ))) ; theorem :: TEX_4:75 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "y")) ")" ))) "or" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "y")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "y")) ")" )) "#)" )) ")" ))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_tex_4 :::"maximal_anti-discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set ($#k5_tex_4 :::"MaxADSspace"::: ) "x") -> ($#v1_pre_topc :::"strict"::: ) ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ; end; theorem :: TEX_4:76 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")))) "holds" (Bool (Set ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))))) ; theorem :: TEX_4:77 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")))) "holds" (Bool (Set ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))))) ; theorem :: TEX_4:78 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k1_tex_2 :::"Sspace"::: ) (Set (Var "x"))) "is" ($#v4_tex_4 :::"maximal_anti-discrete"::: ) ))) ; notationlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); synonym :::"Sspace"::: "A" for "Y" :::"|"::: "A"; end; theorem :: TEX_4:79 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_pre_topc :::"Sspace"::: ) (Set (Var "A")) ")" )))) ; theorem :: TEX_4:80 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")))) "holds" (Bool (Set ($#k1_pre_topc :::"Sspace"::: ) (Set (Var "A"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y0")))))) ; registrationlet "Y" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_pre_topc :::"strict"::: ) ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y"; end; registrationlet "Y" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k1_pre_topc :::"Sspace"::: ) "A") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k1_pre_topc :::"Sspace"::: ) "A") -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) ; end; definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); func :::"MaxADSspace"::: "A" -> ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y" means :: TEX_4:def 18 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) "A")); end; :: deftheorem defines :::"MaxADSspace"::: TEX_4:def 18 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")))) ")" )))); registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k6_tex_4 :::"MaxADSspace"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: TEX_4:81 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")) ")" )))) ; theorem :: TEX_4:82 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_pre_topc :::"Sspace"::: ) (Set (Var "A"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")))))) ; theorem :: TEX_4:83 (Bool "for" (Set (Var "Y")) "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 "Y")) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k5_tex_4 :::"MaxADSspace"::: ) (Set (Var "x")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "#)" )))) ; theorem :: TEX_4:84 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "B")))))) ; theorem :: TEX_4:85 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" ) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" ) ")" )) "#)" )))) ; theorem :: TEX_4:86 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "B")) ")" ))) "holds" (Bool (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "B")))))) ; theorem :: TEX_4:87 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")) ")" )) & (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "B")) ")" )) ")" ) "iff" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "B")) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "B")) ")" )) "#)" )) ")" ))) ; registrationlet "Y" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k6_tex_4 :::"MaxADSspace"::: ) "A") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#~v1_subset_1 "non" ($#v1_subset_1 :::"proper"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); cluster (Set ($#k6_tex_4 :::"MaxADSspace"::: ) "A") -> ($#v1_pre_topc :::"strict"::: ) ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) ; end; theorem :: TEX_4:88 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")))) "holds" (Bool (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))))) ; theorem :: TEX_4:89 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")))) "holds" (Bool (Set ($#k6_tex_4 :::"MaxADSspace"::: ) (Set (Var "A"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))))) ;