:: TDLAT_3 semantic presentation begin theorem :: TDLAT_3:1 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: TDLAT_3:2 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "C")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: TDLAT_3:3 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: TDLAT_3:4 (Bool "for" (Set (Var "X")) "being" ($#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 (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; theorem :: TDLAT_3:5 (Bool "for" (Set (Var "X")) "being" ($#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" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")))) ")" ))) ; theorem :: TDLAT_3:6 (Bool "for" (Set (Var "X")) "being" ($#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" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))))) ; theorem :: TDLAT_3:7 (Bool "for" (Set (Var "X")) "being" ($#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" ($#v4_tops_1 :::"condensed"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) ")" ))) ; theorem :: TDLAT_3:8 (Bool "for" (Set (Var "X")) "being" ($#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" ($#v4_tops_1 :::"condensed"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; theorem :: TDLAT_3:9 (Bool "for" (Set (Var "X")) "being" ($#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" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))) ")" ))) ; begin definitionlet "IT" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "IT" is :::"discrete"::: means :: TDLAT_3:def 1 (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT") ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT"))); attr "IT" is :::"anti-discrete"::: means :: TDLAT_3:def 2 (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT") ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#k2_tarski :::"}"::: ) )); end; :: deftheorem defines :::"discrete"::: TDLAT_3:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) "iff" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))))) ")" )); :: deftheorem defines :::"anti-discrete"::: TDLAT_3:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) "iff" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#k2_tarski :::"}"::: ) )) ")" )); theorem :: TDLAT_3:10 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) )) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_tarski :::"}"::: ) ))) ; theorem :: TDLAT_3:11 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) & (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TDLAT_3:12 (Bool "for" (Set (Var "Y")) "being" ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))))) ; theorem :: TDLAT_3:13 (Bool "for" (Set (Var "Y")) "being" ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))))) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))))) ; registration cluster ($#v1_tdlat_3 :::"discrete"::: ) -> ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#v2_pre_topc :::"TopSpace-like"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TDLAT_3:14 (Bool "for" (Set (Var "Y")) "being" ($#v2_pre_topc :::"TopSpace-like"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) ")" )) ; definitionlet "IT" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "IT" is :::"almost_discrete"::: means :: TDLAT_3:def 3 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "IT" "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT"))) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "IT"))); end; :: deftheorem defines :::"almost_discrete"::: TDLAT_3:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT"))))) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "IT"))))) ")" )); registration cluster ($#v1_tdlat_3 :::"discrete"::: ) -> ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#v1_pre_topc :::"strict"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TDLAT_3:15 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) ")" )) ; theorem :: TDLAT_3:16 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" )) ; theorem :: TDLAT_3:17 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) )) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster -> ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tdlat_3 :::"discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TDLAT_3:18 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )) ")" )) ; theorem :: TDLAT_3:19 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )) ")" )) ; theorem :: TDLAT_3:20 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v2_tdlat_3 :::"anti-discrete"::: ) )) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster -> ($#v2_tdlat_3 :::"anti-discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TDLAT_3:21 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" )) ; theorem :: TDLAT_3:22 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) ")" )) ; theorem :: TDLAT_3:23 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ")" )) ; theorem :: TDLAT_3:24 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ")" )) ; registration cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TDLAT_3:25 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) )) ; theorem :: TDLAT_3:26 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ) ")" ) ")" )) ; registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tdlat_3 :::"discrete"::: ) -> ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_tsep_1 :::"open"::: ) -> ($#v1_borsuk_1 :::"closed"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_borsuk_1 :::"closed"::: ) -> ($#v1_tsep_1 :::"open"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; begin definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "IT" is :::"extremally_disconnected"::: means :: TDLAT_3:def 4 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "IT" "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) )); end; :: deftheorem defines :::"extremally_disconnected"::: TDLAT_3:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TDLAT_3:27 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" )) ; theorem :: TDLAT_3:28 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B"))))) ")" )) ; theorem :: TDLAT_3:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) ")" )) ; theorem :: TDLAT_3:30 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )))) ")" )) ; theorem :: TDLAT_3:31 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )))) ")" )) ; theorem :: TDLAT_3:32 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" )) ; theorem :: TDLAT_3:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) ")" )) ")" )) ; theorem :: TDLAT_3:34 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )))) ")" )) ; theorem :: TDLAT_3:35 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))))) ")" )) ; theorem :: TDLAT_3:36 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) "is" ($#v6_tops_1 :::"open_condensed"::: ) )) "implies" (Bool (Set (Var "A")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "A")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) )) "implies" (Bool (Set (Var "A")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) ")" ")" )) ")" )) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "IT" is :::"hereditarily_extremally_disconnected"::: means :: TDLAT_3:def 5 (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "IT" "holds" (Bool (Set (Var "X0")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) )); end; :: deftheorem defines :::"hereditarily_extremally_disconnected"::: TDLAT_3:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) ) "iff" (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "X0")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TDLAT_3:37 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "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 "X0")))) & (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Var "X0")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TDLAT_3:38 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (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")) "holds" (Bool (Set (Var "X0")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v5_tdlat_3 :::"hereditarily_extremally_disconnected"::: ) )) ; begin theorem :: TDLAT_3:39 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_tdlat_1 :::"Domains_of"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_tdlat_1 :::"Closed_Domains_of"::: ) (Set (Var "Y"))))) ; theorem :: TDLAT_3:40 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_tdlat_1 :::"D-Union"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_tdlat_1 :::"CLD-Union"::: ) (Set (Var "Y")))) & (Bool (Set ($#k3_tdlat_1 :::"D-Meet"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_tdlat_1 :::"CLD-Meet"::: ) (Set (Var "Y")))) ")" )) ; theorem :: TDLAT_3:41 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_tdlat_1 :::"Closed_Domains_Lattice"::: ) (Set (Var "Y"))))) ; theorem :: TDLAT_3:42 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_tdlat_1 :::"Domains_of"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k9_tdlat_1 :::"Open_Domains_of"::: ) (Set (Var "Y"))))) ; theorem :: TDLAT_3:43 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_tdlat_1 :::"D-Union"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k10_tdlat_1 :::"OPD-Union"::: ) (Set (Var "Y")))) & (Bool (Set ($#k3_tdlat_1 :::"D-Meet"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_tdlat_1 :::"OPD-Meet"::: ) (Set (Var "Y")))) ")" )) ; theorem :: TDLAT_3:44 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k12_tdlat_1 :::"Open_Domains_Lattice"::: ) (Set (Var "Y"))))) ; theorem :: TDLAT_3:45 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_tdlat_1 :::"Domains_of"::: ) (Set (Var "Y"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_tdlat_1 :::"D-Union"::: ) (Set (Var "Y")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Set "(" ($#k3_tdlat_1 :::"D-Meet"::: ) (Set (Var "Y")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")))) ")" ))) ; theorem :: TDLAT_3:46 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_tdlat_1 :::"Domains_of"::: ) (Set (Var "Y"))) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B")))) ")" )))) ; theorem :: TDLAT_3:47 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tdlat_2 :::"domains-family"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "S")) "," (Set "(" ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" )))))) ; theorem :: TDLAT_3:48 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tdlat_2 :::"domains-family"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "S")) "," (Set "(" ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "S")) "," (Set "(" ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "Y")))) ")" ")" )))) ; theorem :: TDLAT_3:49 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool (Set ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "X"))) "is" ($#l3_lattices :::"M_Lattice":::)) ")" )) ; theorem :: TDLAT_3:50 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k8_tdlat_1 :::"Closed_Domains_Lattice"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) )) ; theorem :: TDLAT_3:51 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k12_tdlat_1 :::"Open_Domains_Lattice"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) )) ; theorem :: TDLAT_3:52 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) )) ; theorem :: TDLAT_3:53 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_tdlat_3 :::"extremally_disconnected"::: ) ) "iff" (Bool (Set ($#k4_tdlat_1 :::"Domains_Lattice"::: ) (Set (Var "X"))) "is" ($#l3_lattices :::"B_Lattice":::)) ")" )) ;