:: TSEP_1 semantic presentation begin theorem :: TSEP_1:1 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:2 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set (Var "X")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")))) ; theorem :: TSEP_1:3 (Bool "for" (Set (Var "X")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: TSEP_1:4 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) "iff" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) ")" ))) ; theorem :: TSEP_1:5 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X2"))) "#)" )))) ; theorem :: TSEP_1:6 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X2"))) "#)" )))) ; theorem :: TSEP_1:7 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")))))) ; theorem :: TSEP_1:8 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))))) ; theorem :: TSEP_1:9 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))))) ; theorem :: TSEP_1:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))))) ; theorem :: TSEP_1:11 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#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"))))) "holds" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; theorem :: TSEP_1:12 (Bool "for" (Set (Var "X")) "being" ($#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" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))))) ; theorem :: TSEP_1:13 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X2")) "being" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "X2")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")))))) ; theorem :: TSEP_1:14 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "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 "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set (Var "X1")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))))) ; theorem :: TSEP_1:15 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))))) ; definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); attr "IT" is :::"open"::: means :: TSEP_1:def 1 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT"))) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )); end; :: deftheorem defines :::"open"::: TSEP_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tsep_1 :::"open"::: ) ) "iff" (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 "IT"))))) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))); registrationlet "X" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tsep_1 :::"open"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; 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_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tsep_1 :::"open"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TSEP_1:16 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#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"))))) "holds" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )))) ; theorem :: TSEP_1:17 (Bool "for" (Set (Var "X")) "being" ($#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" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))))) ; theorem :: TSEP_1:18 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X2")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "X2")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")))))) ; theorem :: TSEP_1:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))))) ; theorem :: TSEP_1:20 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))))) ; begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "X1", "X2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); func "X1" :::"union"::: "X2" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "X" means :: TSEP_1:def 2 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X2"))); commutativity (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))))) ; end; :: deftheorem defines :::"union"::: TSEP_1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) ")" )))); theorem :: TSEP_1:21 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set "(" (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X3")) ")" ))))) ; theorem :: TSEP_1:22 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))))) ; theorem :: TSEP_1:23 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) "iff" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X2"))) "#)" )) ")" ))) ; theorem :: TSEP_1:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:25 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; definitionlet "X1", "X2" be ($#l1_struct_0 :::"1-sorted"::: ) ; pred "X1" :::"misses"::: "X2" means :: TSEP_1:def 3 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1") ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X2")); symmetry (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) ; end; :: deftheorem defines :::"misses"::: TSEP_1:def 3 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) ")" )); notationlet "X1", "X2" be ($#l1_struct_0 :::"1-sorted"::: ) ; antonym "X1" :::"meets"::: "X2" for "X1" :::"misses"::: "X2"; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "X1", "X2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); assume (Bool (Set (Const "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Const "X2"))) ; func "X1" :::"meet"::: "X2" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "X" means :: TSEP_1:def 4 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1") ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X2"))); end; :: deftheorem defines :::"meet"::: TSEP_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) ")" )))); theorem :: TSEP_1:26 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1")))) ")" & "(" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X3"))) ")" ) "or" (Bool "(" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X3"))) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3")))) ")" ) ")" )) "implies" (Bool (Set (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3")) ")" ))) ")" ")" ))) ; theorem :: TSEP_1:27 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) ")" ))) ; theorem :: TSEP_1:28 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" )) ")" & "(" (Bool (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" ))) "implies" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) ")" & "(" (Bool (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X2"))) "#)" )) ")" & "(" (Bool (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X2"))) "#)" ))) "implies" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) ")" ")" ))) ; theorem :: TSEP_1:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:30 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:31 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))))) ; theorem :: TSEP_1:32 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set "(" (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set "(" (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ))) ")" ))) ; theorem :: TSEP_1:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y")) ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set (Set (Var "Y")) ($#k1_tsep_1 :::"union"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X1")) ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "Y")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ))) ")" ))) ; begin notationlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); antonym "A1" "," "A2" :::"are_not_separated"::: for "A1" "," "A2" :::"are_separated"::: ; end; theorem :: TSEP_1:34 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) "iff" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:35 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; theorem :: TSEP_1:36 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A1")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")))))) ; theorem :: TSEP_1:37 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) "iff" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:38 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; theorem :: TSEP_1:39 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C"))) "," (Set (Set (Var "A2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C"))) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_1:40 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ) "or" (Bool (Set (Var "A2")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2"))) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_1:41 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:42 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "C1"))) & (Bool (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "C2"))) & (Bool (Set (Var "C1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Var "C2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A1"))) & (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:43 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "C1"))) & (Bool (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "C2"))) & (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:44 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "C1"))) & (Bool (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "C2"))) & (Bool (Set (Var "C1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Var "C2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A1"))) & (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:45 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "C1"))) & (Bool (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "C2"))) & (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" ))) ; definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); pred "A1" "," "A2" :::"are_weakly_separated"::: means :: TSEP_1:def 5 (Bool (Set "A1" ($#k7_subset_1 :::"\"::: ) "A2") "," (Set "A2" ($#k7_subset_1 :::"\"::: ) "A1") ($#r1_connsp_1 :::"are_separated"::: ) ); symmetry (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2"))) "," (Set (Set (Var "A2")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Set (Var "A2")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) "," (Set (Set (Var "A1")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2"))) ($#r1_connsp_1 :::"are_separated"::: ) )) ; end; :: deftheorem defines :::"are_weakly_separated"::: TSEP_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool (Set (Set (Var "A1")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2"))) "," (Set (Set (Var "A2")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))); notationlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); antonym "A1" "," "A2" :::"are_not_weakly_separated"::: for "A1" "," "A2" :::"are_weakly_separated"::: ; end; theorem :: TSEP_1:46 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) ")" ) "iff" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:47 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:48 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:49 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:50 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C"))) "," (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C"))) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:51 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A2")) "," (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "B2")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B1"))) "," (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2"))) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:52 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "B")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "B")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2"))) "," (Set (Var "B")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:53 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "B")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "B")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) "," (Set (Var "B")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:54 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "C2")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:55 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) & (Bool (Bool "not" (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))))) "holds" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "C2")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")))) "or" (Bool "ex" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) ")" )) ")" ) ")" )))) ; theorem :: TSEP_1:56 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:57 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) & (Bool (Bool "not" (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))))) "holds" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")))) "or" (Bool "ex" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" ) ")" )))) ; theorem :: TSEP_1:58 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "C2")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:59 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) & (Bool (Bool "not" (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))))) "holds" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "C2")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")))) "or" (Bool "ex" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) ")" )) ")" ) ")" )))) ; theorem :: TSEP_1:60 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ")" ))) ; theorem :: TSEP_1:61 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) & (Bool (Bool "not" (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))))) "holds" (Bool "ex" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")))) "or" (Bool "ex" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ")" ) ")" )))) ; theorem :: TSEP_1:62 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "B1"))) & (Bool (Set (Var "A2")) ($#r1_tarski :::"c="::: ) (Set (Var "B2"))) & (Bool (Set (Set (Var "B1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B2"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) ")" )) ")" ))) ; begin definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "X1", "X2" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); pred "X1" "," "X2" :::"are_separated"::: means :: TSEP_1:def 6 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1")) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X2"))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )); symmetry (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")) "st" (Bool (Bool "(" "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; end; :: deftheorem defines :::"are_separated"::: TSEP_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )) ")" ))); notationlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "X1", "X2" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); antonym "X1" "," "X2" :::"are_not_separated"::: for "X1" "," "X2" :::"are_separated"::: ; end; theorem :: TSEP_1:63 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))))) ; theorem :: TSEP_1:64 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "iff" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:65 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:66 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:67 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "iff" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:68 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:69 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TSEP_1:70 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y"))) "," (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y"))) ($#r3_tsep_1 :::"are_separated"::: ) ) & (Bool (Set (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1"))) "," (Set (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:71 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r3_tsep_1 :::"are_separated"::: ) )))) ; theorem :: TSEP_1:72 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "," (Set (Var "Y")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "," (Set (Var "Y")) ($#r3_tsep_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_1:73 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "Y")) ($#r3_tsep_1 :::"are_separated"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y")) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "," (Set (Var "Y")) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:74 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y2"))) & (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) ")" )) ")" ))) ; theorem :: TSEP_1:75 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y2"))) & (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Y2"))) "or" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ) ")" )) ")" ))) ; theorem :: TSEP_1:76 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y2"))) & (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) ")" )) ")" ))) ; theorem :: TSEP_1:77 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y2"))) & (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Y2"))) "or" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ) ")" )) ")" ))) ; definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "X1", "X2" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); pred "X1" "," "X2" :::"are_weakly_separated"::: means :: TSEP_1:def 7 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1")) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X2"))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )); symmetry (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")) "st" (Bool (Bool "(" "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; end; :: deftheorem defines :::"are_weakly_separated"::: TSEP_1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) ")" ))); notationlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "X1", "X2" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); antonym "X1" "," "X2" :::"are_not_weakly_separated"::: for "X1" "," "X2" :::"are_weakly_separated"::: ; end; theorem :: TSEP_1:78 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" ) "iff" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:79 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:80 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:81 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:82 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y"))) "," (Set (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y"))) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_1:83 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X2")) "," (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y1"))) "," (Set (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X1"))) "," (Set (Set (Var "Y2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" ))) ; theorem :: TSEP_1:84 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "," (Set (Var "Y")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "," (Set (Var "Y")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" & "(" (Bool (Bool (Set (Var "Y")) "," (Set (Var "X1")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "Y")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "implies" (Bool (Set (Var "Y")) "," (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" ")" ))) ; theorem :: TSEP_1:85 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "," (Set (Var "Y")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "implies" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "," (Set (Var "Y")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" & "(" (Bool (Bool (Set (Var "Y")) "," (Set (Var "X1")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "Y")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "implies" (Bool (Set (Var "Y")) "," (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" ")" ))) ; theorem :: TSEP_1:86 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) "or" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Set (Var "Y2")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool "(" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")))) "or" (Bool "ex" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" )) ")" ) ")" )) ")" ) ")" ))) ; theorem :: TSEP_1:87 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) "or" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")))) "or" (Bool "ex" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y")))) & (Bool (Set (Var "Y")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" )) ")" ) ")" )) ")" ) ")" ))) ; theorem :: TSEP_1:88 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X2")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" ) ")" ))) ; theorem :: TSEP_1:89 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) "or" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Set (Var "Y2")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool "(" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")))) "or" (Bool "ex" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "Y")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" )) ")" ) ")" )) ")" ) ")" ))) ; theorem :: TSEP_1:90 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) "or" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")))) "or" (Bool "ex" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y")))) & (Bool (Set (Var "Y")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" )) ")" ) ")" )) ")" ) ")" ))) ; theorem :: TSEP_1:91 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X2")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" ) ")" ))) ; theorem :: TSEP_1:92 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "ex" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) & (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y2"))) & (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Y2"))) "or" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ) ")" )) ")" ))) ; theorem :: TSEP_1:93 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" ))) ;