:: TOPS_3 semantic presentation begin theorem :: TOPS_3:1 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X"))))) "implies" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))) ; theorem :: TOPS_3:2 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))))) "implies" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X"))))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "implies" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" ")" ))) ; theorem :: TOPS_3:3 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ))))) ; theorem :: TOPS_3:4 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ))))) ; theorem :: TOPS_3:5 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ))))) ; theorem :: TOPS_3:6 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: TOPS_3:7 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPS_3:8 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; begin definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"boundary"::: means :: TOPS_3:def 1 (Bool (Set ($#k1_tops_1 :::"Int"::: ) "A") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"boundary"::: TOPS_3:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); theorem :: TOPS_3:9 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X"))) "is" ($#v2_tops_1 :::"boundary"::: ) )) ; theorem :: TOPS_3: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")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; theorem :: TOPS_3:11 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ))) ; theorem :: TOPS_3:12 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) ")" ))) ; theorem :: TOPS_3:13 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "G")))) ")" ))) ; theorem :: TOPS_3:14 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A")) ")" )))) ")" ))) ; theorem :: TOPS_3:15 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v2_tops_1 :::"boundary"::: ) ))) ; definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"dense"::: means :: TOPS_3:def 2 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) "A") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; :: deftheorem defines :::"dense"::: TOPS_3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" ))); theorem :: TOPS_3:16 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))) "is" ($#v1_tops_1 :::"dense"::: ) )) ; theorem :: TOPS_3:17 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPS_3:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_tops_1 :::"boundary"::: ) ) ")" ))) ; theorem :: TOPS_3:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) ")" ))) ; theorem :: TOPS_3:20 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "G")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" )))) ")" ))) ; theorem :: TOPS_3:21 (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")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"nowhere_dense"::: means :: TOPS_3:def 3 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"nowhere_dense"::: TOPS_3:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); theorem :: TOPS_3:22 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "X"))) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) ; theorem :: TOPS_3:23 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))) ; theorem :: TOPS_3:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; theorem :: TOPS_3:25 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) )))) ; theorem :: TOPS_3:26 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; theorem :: TOPS_3:27 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) "is" ($#v2_tops_1 :::"boundary"::: ) ) ")" )) ")" ))) ; theorem :: TOPS_3:28 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "H")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "H"))) ")" ))) ")" ))) ; theorem :: TOPS_3:29 (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")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; theorem :: TOPS_3:30 (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")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v2_tops_1 :::"boundary"::: ) ))) ; definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "A" is :::"everywhere_dense"::: means :: TOPS_3:def 4 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "X")); end; :: deftheorem defines :::"everywhere_dense"::: TOPS_3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))) ")" ))); definitionlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "A" is :::"everywhere_dense"::: means :: TOPS_3:def 5 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; :: deftheorem defines :::"everywhere_dense"::: TOPS_3:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" ))); theorem :: TOPS_3:31 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) ; theorem :: TOPS_3:32 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))) ; theorem :: TOPS_3:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; theorem :: TOPS_3:34 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPS_3:35 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))) ; theorem :: TOPS_3:36 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))) ; theorem :: TOPS_3:37 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) )))) ; theorem :: TOPS_3:38 (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")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))) ; theorem :: TOPS_3:39 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) ")" ))) ; theorem :: TOPS_3:40 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ))) ; theorem :: TOPS_3:41 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" )) ")" ))) ; theorem :: TOPS_3:42 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "H")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" ))) ")" ))) ; theorem :: TOPS_3:43 (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")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))) ; theorem :: TOPS_3:44 (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")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))) ; theorem :: TOPS_3:45 (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")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; theorem :: TOPS_3:46 (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")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; theorem :: TOPS_3:47 (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")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; theorem :: TOPS_3:48 (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")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))) ; theorem :: TOPS_3:49 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) & (Bool (Set (Set (Var "C")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) ")" )))) ; theorem :: TOPS_3:50 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Set (Var "C")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "D")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "C")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )))) ; theorem :: TOPS_3:51 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "C")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )))) ; theorem :: TOPS_3:52 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool "ex" (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "D")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "C")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "C")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )))) ; begin theorem :: TOPS_3:53 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#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 "Y0")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))))))) ; theorem :: TOPS_3:54 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")))))))) ; theorem :: TOPS_3:55 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")))))))) ; theorem :: TOPS_3:56 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#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 "Y0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")))))))) ; theorem :: TOPS_3:57 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")))))))) ; theorem :: TOPS_3:58 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")))))))) ; theorem :: TOPS_3:59 (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")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) ))))) ; theorem :: TOPS_3:60 (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 "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))))) ; theorem :: TOPS_3:61 (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 "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_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ))))) ; theorem :: TOPS_3:62 (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 "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ))))) ; theorem :: TOPS_3:63 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ))))) ; theorem :: TOPS_3:64 (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 "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ) "iff" (Bool (Set (Var "A")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) ) ")" ))))) ; theorem :: TOPS_3:65 (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 "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_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ))))) ; theorem :: TOPS_3:66 (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 "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) ))))) ; theorem :: TOPS_3:67 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "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 "A")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v2_tops_1 :::"boundary"::: ) ) ")" ))))) ; theorem :: TOPS_3:68 (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 "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_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))))) ; theorem :: TOPS_3:69 (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 "C")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))))) ; theorem :: TOPS_3:70 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "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 "A")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) ")" ))))) ; begin theorem :: TOPS_3:71 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))))) "holds" (Bool "for" (Set (Var "C1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "holds" (Bool "(" (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2"))) "iff" (Bool (Set (Set (Var "C1")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "C2")) ($#k3_subset_1 :::"`"::: ) )) ")" )))) ; theorem :: TOPS_3:72 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool "(" "for" (Set (Var "C1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))) "holds" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Var "C2")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" )) "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 :: TOPS_3:73 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool "(" "for" (Set (Var "C1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))) "holds" (Bool "(" (Bool (Set (Var "C1")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Var "C2")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) ")" )) "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 :: TOPS_3:74 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool "(" "for" (Set (Var "C1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "C2"))))) ")" )) "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 :: TOPS_3:75 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool "(" "for" (Set (Var "C1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C2"))))) ")" )) "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 :: TOPS_3:76 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_hidden :::"="::: ) (Set (Var "D2"))) & (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"))) "#)" )) & (Bool (Set (Var "D1")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "D2")) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: TOPS_3:77 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_hidden :::"="::: ) (Set (Var "D2"))) & (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"))) "#)" ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "D2"))))))) ; theorem :: TOPS_3:78 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2"))) & (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"))) "#)" ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "D1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "D2"))))))) ; theorem :: TOPS_3:79 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_hidden :::"="::: ) (Set (Var "D2"))) & (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"))) "#)" )) & (Bool (Set (Var "D1")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "D2")) "is" ($#v4_pre_topc :::"closed"::: ) )))) ; theorem :: TOPS_3:80 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_hidden :::"="::: ) (Set (Var "D2"))) & (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"))) "#)" ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "D2"))))))) ; theorem :: TOPS_3:81 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2"))) & (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"))) "#)" ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "D1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "D2"))))))) ; theorem :: TOPS_3:82 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D2")) ($#r1_tarski :::"c="::: ) (Set (Var "D1"))) & (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"))) "#)" )) & (Bool (Set (Var "D1")) "is" ($#v2_tops_1 :::"boundary"::: ) )) "holds" (Bool (Set (Var "D2")) "is" ($#v2_tops_1 :::"boundary"::: ) )))) ; theorem :: TOPS_3:83 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2"))) & (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"))) "#)" )) & (Bool (Set (Var "D1")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool (Set (Var "D2")) "is" ($#v1_tops_1 :::"dense"::: ) )))) ; theorem :: TOPS_3:84 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D2")) ($#r1_tarski :::"c="::: ) (Set (Var "D1"))) & (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"))) "#)" )) & (Bool (Set (Var "D1")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Var "D2")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )))) ; theorem :: TOPS_3:85 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2"))) & (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"))) "#)" )) & (Bool (Set (Var "D1")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )) "holds" (Bool (Set (Var "D2")) "is" ($#v1_tops_3 :::"everywhere_dense"::: ) )))) ;