:: TSEP_2 semantic presentation begin theorem :: TSEP_2:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))))) ; definitionlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); pred "A1" "," "A2" :::"constitute_a_decomposition"::: means :: TSEP_2:def 1 (Bool "(" (Bool "A1" ($#r1_xboole_0 :::"misses"::: ) "A2") & (Bool (Set "A1" ($#k4_subset_1 :::"\/"::: ) "A2") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) ")" ); symmetry (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))))) "holds" (Bool "(" (Bool (Set (Var "A2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A1"))) & (Bool (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X")))) ")" )) ; end; :: deftheorem defines :::"constitute_a_decomposition"::: TSEP_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (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_tsep_2 :::"constitute_a_decomposition"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" ) ")" ))); notationlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); antonym "A1" "," "A2" :::"do_not_constitute_a_decomposition"::: for "A1" "," "A2" :::"constitute_a_decomposition"::: ; end; theorem :: TSEP_2:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (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_tsep_2 :::"constitute_a_decomposition"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))) ")" ) ")" ))) ; theorem :: TSEP_2:3 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (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")) ($#r1_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_subset_1 :::"`"::: ) )) ")" ))) ; theorem :: TSEP_2:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k3_subset_1 :::"`"::: ) )) "or" (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_subset_1 :::"`"::: ) )) ")" )) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_tsep_2 :::"constitute_a_decomposition"::: ) ))) ; theorem :: TSEP_2:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "A")) "," (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tsep_2 :::"constitute_a_decomposition"::: ) ))) ; theorem :: TSEP_2:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X"))) "," (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))) ($#r1_tsep_2 :::"constitute_a_decomposition"::: ) )) ; theorem :: TSEP_2:7 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "A")) "," (Set (Var "A")) ($#r1_tsep_2 :::"do_not_constitute_a_decomposition"::: ) ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); :: original: :::"constitute_a_decomposition"::: redefine pred "A1" "," "A2" :::"constitute_a_decomposition"::: ; irreflexivity (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")) "holds" (Bool ((Set (Const "X")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: TSEP_2:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A")) "," (Set (Var "A2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2"))))) ; theorem :: TSEP_2:9 (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_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1"))) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A2"))) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A1"))) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2"))) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) ")" ))) ; theorem :: TSEP_2:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) ")" ))) ; theorem :: TSEP_2:11 (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_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "A2")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; theorem :: TSEP_2:12 (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_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Var "A2")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; theorem :: TSEP_2:13 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B1"))) "," (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2"))) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ))) ; theorem :: TSEP_2:14 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B1"))) "," (Set (Set (Var "A2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B2"))) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ))) ; begin theorem :: TSEP_2:15 (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")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "C1")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "C2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) ")" ))) ; theorem :: TSEP_2:16 (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 (Set (Set (Var "A1")) ($#k3_subset_1 :::"`"::: ) ) "," (Set (Set (Var "A2")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) ")" ))) ; theorem :: TSEP_2:17 (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")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "C1")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "C2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:18 (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")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "C1")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "C2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_2:19 (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")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "C1")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "A2")) "," (Set (Var "C2")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_2:20 (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_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (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_2:21 (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 (Set (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) "," (Set (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2"))) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_2:22 (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")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:23 (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 (Set (Set (Var "A1")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) "," (Set (Set (Var "A2")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))) ; theorem :: TSEP_2:24 (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")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "A1"))) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:25 (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")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) ) "iff" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r1_connsp_1 :::"are_separated"::: ) ) ")" ))))) ; theorem :: TSEP_2:26 (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")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A1")))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r1_connsp_1 :::"are_separated"::: ) ))))) ; theorem :: TSEP_2:27 (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")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set (Var "A2")))) "holds" (Bool "(" (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ) ")" ))))) ; theorem :: TSEP_2:28 (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")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A1")))) & (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "B1")) "," (Set (Var "B2")) ($#r2_tsep_1 :::"are_weakly_separated"::: ) ))))) ; begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X1", "X2" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); pred "X1" "," "X2" :::"constitute_a_decomposition"::: means :: TSEP_2:def 2 (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_2 :::"constitute_a_decomposition"::: ) )); 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_2 :::"constitute_a_decomposition"::: ) ) ")" )) "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_2 :::"constitute_a_decomposition"::: ) ))) ; end; :: deftheorem defines :::"constitute_a_decomposition"::: TSEP_2:def 2 : (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" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) ) "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_2 :::"constitute_a_decomposition"::: ) )) ")" ))); notationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X1", "X2" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); antonym "X1" "," "X2" :::"do_not_constitute_a_decomposition"::: for "X1" "," "X2" :::"constitute_a_decomposition"::: ; end; theorem :: TSEP_2: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"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (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 (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ) ")" ))) ; theorem :: TSEP_2:30 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X0")) "," (Set (Var "X0")) ($#r3_tsep_2 :::"do_not_constitute_a_decomposition"::: ) ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A1", "A2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); :: original: :::"constitute_a_decomposition"::: redefine pred "A1" "," "A2" :::"constitute_a_decomposition"::: ; irreflexivity (Bool "for" (Set (Var "A1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")) "holds" (Bool ((Set (Const "X")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: TSEP_2: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 "X0")) "," (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 "X0")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X0")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )) "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_2: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 "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 "X1")) "," (Set (Var "Y1")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) ($#r1_hidden :::"="::: ) (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"))) "#)" )) "iff" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) ")" ))) ; theorem :: TSEP_2: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")) "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_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ) "iff" (Bool (Set (Var "X2")) "is" ($#v1_borsuk_1 :::"closed"::: ) ) ")" ))) ; theorem :: TSEP_2:34 (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")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ) "iff" (Bool (Set (Var "X2")) "is" ($#v1_tsep_1 :::"open"::: ) ) ")" ))) ; theorem :: TSEP_2:35 (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 "Y1")) "," (Set (Var "X2")) "," (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 "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y1"))) "," (Set (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ))) ; theorem :: TSEP_2:36 (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 "Y2")) "," (Set (Var "X1")) "," (Set (Var "Y1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y2"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y1"))) "," (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ))) ; begin theorem :: TSEP_2:37 (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 "Y1")) "," (Set (Var "Y2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "Y1")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:38 (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 "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 "X1")) "," (Set (Var "Y1")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:39 (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 "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 "X1")) "," (Set (Var "Y1")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_2:40 (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 "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 "X1")) "," (Set (Var "Y1")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) ($#r1_hidden :::"="::: ) (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"))) "#)" )) & (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ))) ; theorem :: TSEP_2:41 (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")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (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_2:42 (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 "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 "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:43 (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 "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 "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y2"))) & (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ))) ; theorem :: TSEP_2:44 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y2"))))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r3_tsep_1 :::"are_separated"::: ) ) ")" ))))) ; theorem :: TSEP_2:45 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (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 "X0"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "Y1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) & (Bool (Set (Var "Y2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) & (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_2:46 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y2"))))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) "iff" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) ) ")" ))))) ; theorem :: TSEP_2:47 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (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 "X0"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "Y1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) & (Bool (Set (Var "Y2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )))) ;