:: TEX_3 semantic presentation begin theorem :: TEX_3:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "B")) "is" ($#v1_subset_1 :::"proper"::: ) ) ")" ))) ; theorem :: TEX_3:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) ) ")" ))) ; theorem :: TEX_3:3 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))) ; theorem :: TEX_3:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) ")" ))) ; theorem :: TEX_3:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ))) ; theorem :: TEX_3:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (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_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#v1_tex_2 :::"proper"::: ) ) & (Bool (Set (Var "Y2")) "is" ($#v1_tex_2 :::"proper"::: ) ) ")" ))) ; theorem :: TEX_3:7 (Bool "for" (Set (Var "X")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))))) ; theorem :: TEX_3:8 (Bool "for" (Set (Var "X")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_2 :::"proper"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "Y1")) "," (Set (Var "Y2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); attr "IT" is :::"dense"::: means :: TEX_3: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" ($#v1_tops_1 :::"dense"::: ) )); end; :: deftheorem defines :::"dense"::: TEX_3:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tex_3 :::"dense"::: ) ) "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" ($#v1_tops_1 :::"dense"::: ) )) ")" ))); theorem :: TEX_3:9 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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_tex_3 :::"dense"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tex_3 :::"dense"::: ) -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) -> ($#~v1_borsuk_1 "non" ($#v1_borsuk_1 :::"closed"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tex_2 :::"proper"::: ) -> ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) 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_tex_3 :::"dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:10 (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" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_3 :::"dense"::: ) ($#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 :: TEX_3:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_3 :::"dense"::: ) ($#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" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))))) ; theorem :: TEX_3:12 (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_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (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")))) "holds" (Bool (Set (Var "X2")) "is" ($#v1_tex_3 :::"dense"::: ) )))) ; theorem :: TEX_3:13 (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_tex_3 :::"dense"::: ) ($#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 (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool (Set (Var "X1")) "is" ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))))) ; theorem :: TEX_3: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_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "X2")) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")))))) ; theorem :: TEX_3:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "Y2")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "Y2")) "is" ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" )) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); attr "IT" is :::"everywhere_dense"::: means :: TEX_3:def 2 (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" ($#v1_tops_3 :::"everywhere_dense"::: ) )); end; :: deftheorem defines :::"everywhere_dense"::: TEX_3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) "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" ($#v1_tops_3 :::"everywhere_dense"::: ) )) ")" ))); theorem :: TEX_3:16 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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" ($#v2_tex_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v2_tex_3 :::"everywhere_dense"::: ) -> ($#v1_tex_3 :::"dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) -> ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) -> ($#v2_tex_3 :::"everywhere_dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) -> ($#v1_tex_2 :::"proper"::: ) 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"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:17 (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" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#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 :: TEX_3:18 (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"::: ) ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#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" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ))))) ; theorem :: TEX_3: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" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (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")))) "holds" (Bool (Set (Var "X2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) )))) ; theorem :: TEX_3:20 (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"::: ) ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#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 (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool (Set (Var "X1")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))))) ; theorem :: TEX_3:21 (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"::: ) ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "X2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")))))) ; theorem :: TEX_3:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "Y2")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "Y2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" )) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_3 :::"dense"::: ) -> ($#v2_tex_3 :::"everywhere_dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_3 :::"dense"::: ) ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) -> ($#~v1_tsep_1 "non" ($#v1_tsep_1 :::"open"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tsep_1 :::"open"::: ) ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) -> ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) 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"::: ) ($#v1_tex_3 :::"dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:23 (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" ($#v1_tops_1 :::"dense"::: ) ) & (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"::: ) ($#v1_tex_3 :::"dense"::: ) ($#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 :: TEX_3:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) "iff" (Bool "ex" (Set (Var "X1")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) ")" ))) ; theorem :: TEX_3: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"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tex_3 :::"dense"::: ) ) "or" (Bool (Set (Var "X2")) "is" ($#v1_tex_3 :::"dense"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TEX_3: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")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) "or" (Bool (Set (Var "X2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TEX_3: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")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TEX_3: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 "(" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v1_tex_3 :::"dense"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tex_3 :::"dense"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); attr "IT" is :::"boundary"::: means :: TEX_3:def 3 (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" ($#v2_tops_1 :::"boundary"::: ) )); end; :: deftheorem defines :::"boundary"::: TEX_3:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_tex_3 :::"boundary"::: ) ) "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" ($#v2_tops_1 :::"boundary"::: ) )) ")" ))); theorem :: TEX_3:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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" ($#v3_tex_3 :::"boundary"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tex_3 :::"boundary"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tsep_1 "non" ($#v1_tsep_1 :::"open"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v2_tex_3 :::"everywhere_dense"::: ) -> ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v3_tex_3 :::"boundary"::: ) -> ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:30 (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" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) ")" )))) ; theorem :: TEX_3: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" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tex_3 :::"dense"::: ) ) "iff" (Bool (Set (Var "X2")) "is" ($#v3_tex_3 :::"boundary"::: ) ) ")" ))) ; theorem :: TEX_3: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")) "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" ($#v3_tex_3 :::"boundary"::: ) ) "iff" (Bool (Set (Var "X2")) "is" ($#v1_tex_3 :::"dense"::: ) ) ")" ))) ; theorem :: TEX_3:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) )))) ; theorem :: TEX_3: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" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "holds" (Bool (Set (Var "X2")) "is" ($#v3_tex_3 :::"boundary"::: ) ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); attr "IT" is :::"nowhere_dense"::: means :: TEX_3:def 4 (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_tops_1 :::"nowhere_dense"::: ) )); end; :: deftheorem defines :::"nowhere_dense"::: TEX_3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) "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_tops_1 :::"nowhere_dense"::: ) )) ")" ))); theorem :: TEX_3:35 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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" ($#v4_tex_3 :::"nowhere_dense"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_tex_3 :::"nowhere_dense"::: ) -> ($#v3_tex_3 :::"boundary"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) -> ($#~v4_tex_3 "non" ($#v4_tex_3 :::"nowhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v4_tex_3 :::"nowhere_dense"::: ) -> ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_3 :::"dense"::: ) -> ($#~v4_tex_3 "non" ($#v4_tex_3 :::"nowhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:36 (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_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) ")" )))) ; theorem :: TEX_3: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")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set (Var "X2")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) ")" ))) ; theorem :: TEX_3: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")) "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" ($#v4_tex_3 :::"nowhere_dense"::: ) ) "iff" (Bool (Set (Var "X2")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) ")" ))) ; theorem :: TEX_3:39 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )))) ; theorem :: TEX_3: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")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "holds" (Bool (Set (Var "X2")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) -> ($#v4_tex_3 :::"nowhere_dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v3_tex_3 :::"boundary"::: ) ($#~v4_tex_3 "non" ($#v4_tex_3 :::"nowhere_dense"::: ) ) -> ($#~v1_borsuk_1 "non" ($#v1_borsuk_1 :::"closed"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_borsuk_1 :::"closed"::: ) ($#~v4_tex_3 "non" ($#v4_tex_3 :::"nowhere_dense"::: ) ) -> ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:41 (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" ($#v2_tops_1 :::"boundary"::: ) ) & (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 "(" (Bool (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) ")" )))) ; theorem :: TEX_3:42 (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 "(" (Bool (Set (Var "X0")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) "iff" (Bool "ex" (Set (Var "X1")) "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 "(" (Bool (Set (Var "X1")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) ")" )) ")" ))) ; theorem :: TEX_3: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")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) "is" ($#v3_tex_3 :::"boundary"::: ) ) "or" (Bool (Set (Var "X2")) "is" ($#v3_tex_3 :::"boundary"::: ) ) ")" ) & (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" ($#v3_tex_3 :::"boundary"::: ) ))) ; theorem :: TEX_3:44 (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" ($#v4_tex_3 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ))) ; theorem :: TEX_3:45 (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 "(" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v3_tex_3 :::"boundary"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#v3_tex_3 :::"boundary"::: ) ))) ; theorem :: TEX_3:46 (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 "(" (Bool (Set (Var "X1")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) "or" (Bool (Set (Var "X2")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) ")" ) & (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" ($#v4_tex_3 :::"nowhere_dense"::: ) ))) ; begin theorem :: TEX_3:47 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Bool "not" (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) )) ; theorem :: TEX_3:48 (Bool "for" (Set (Var "X")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "X0")) "being" ($#v1_tex_2 :::"proper"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Bool "not" (Set (Var "X0")) "is" ($#v1_tex_3 :::"dense"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) )) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_2 :::"proper"::: ) -> ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_3 :::"dense"::: ) -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:49 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ))) ; theorem :: TEX_3:50 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_tex_3 :::"dense"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_tex_2 :::"proper"::: ) ) ")" ))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v1_tdlat_3 :::"discrete"::: ) ))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_tex_3 :::"boundary"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:51 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#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" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#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 :: TEX_3:52 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#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 :: TEX_3:53 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; theorem :: TEX_3:54 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; theorem :: TEX_3:55 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "Y2")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "Y2")) "is" ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" ))) ; begin theorem :: TEX_3:56 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Bool "not" (Set (Var "X0")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) )) ; theorem :: TEX_3:57 (Bool "for" (Set (Var "X")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "X0")) "being" ($#v1_tex_2 :::"proper"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Bool "not" (Set (Var "X0")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) )) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) )) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v4_tex_3 "non" ($#v4_tex_3 :::"nowhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_2 :::"proper"::: ) -> ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v2_tex_3 :::"everywhere_dense"::: ) -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tex_3 :::"boundary"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_borsuk_1 "non" ($#v1_borsuk_1 :::"closed"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tex_3 "non" ($#v3_tex_3 :::"boundary"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) -> ($#~v1_tsep_1 "non" ($#v1_tsep_1 :::"open"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_3 :::"dense"::: ) -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) -> ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#~v4_tex_3 "non" ($#v4_tex_3 :::"nowhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#~v2_tex_3 "non" ($#v2_tex_3 :::"everywhere_dense"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:58 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X0")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ))) ; theorem :: TEX_3:59 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_borsuk_1 :::"closed"::: ) ) ")" ))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ))) ; theorem :: TEX_3:60 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v2_tex_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_tex_2 :::"proper"::: ) ) ")" ))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ))) ; theorem :: TEX_3:61 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_tex_3 :::"dense"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_tsep_1 :::"open"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_tex_2 :::"proper"::: ) ) ")" ))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v3_tdlat_3 :::"almost_discrete"::: ) ))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v4_tex_3 :::"nowhere_dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:62 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#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_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v4_tex_3 :::"nowhere_dense"::: ) ($#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 :: TEX_3:63 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#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 :: TEX_3:64 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; theorem :: TEX_3:65 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_2 :::"proper"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; theorem :: TEX_3:66 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "Y2")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "Y1")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "Y2")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" ))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TEX_3:67 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#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" ($#v2_tops_1 :::"boundary"::: ) ) & (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"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#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 :: TEX_3:68 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_subset_1 :::"proper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "A0")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#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 :: TEX_3:69 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; theorem :: TEX_3:70 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) )))) ; theorem :: TEX_3:71 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#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 "(" (Bool (Set (Var "X0")) "is" ($#v4_tex_3 :::"nowhere_dense"::: ) ) "iff" (Bool "ex" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) ")" ))) ; theorem :: TEX_3:72 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v3_tex_3 :::"boundary"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_borsuk_1 :::"closed"::: ) ) ")" ) "or" (Bool "ex" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))(Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (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 "X0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X0"))) "#)" )) & (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 "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" )) ")" ))) ")" ))) ; theorem :: TEX_3:73 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_tex_3 :::"dense"::: ) ) & (Bool (Set (Var "X0")) "is" ($#v1_tsep_1 :::"open"::: ) ) ")" ) "or" (Bool "ex" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))(Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (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 "X0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X0"))) "#)" )) ")" ))) ")" ))) ; theorem :: TEX_3:74 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_tex_3 :::"nowhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))(Bool "ex" (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) ")" ))))) ; theorem :: TEX_3:75 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#v1_tex_2 :::"proper"::: ) ($#v2_tex_3 :::"everywhere_dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X1")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) ($#v1_tex_3 :::"dense"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))(Bool "ex" (Set (Var "X2")) "being" ($#v1_pre_topc :::"strict"::: ) ($#v1_borsuk_1 :::"closed"::: ) ($#v3_tex_3 :::"boundary"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_2 :::"constitute_a_decomposition"::: ) ) & (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) ")" ))))) ;