:: TOPS_1 semantic presentation begin theorem :: TOPS_1:1 (Bool "for" (Set (Var "TS")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Set (Var "K")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "K")) ($#r1_hidden :::"="::: ) (Set (Var "Q"))))) ; theorem :: TOPS_1:2 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "GX")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "GX"))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_pre_topc :::"Cl"::: ) "P") -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: TOPS_1:3 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "R" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "R" ($#k3_subset_1 :::"`"::: ) ) -> ($#v3_pre_topc :::"open"::: ) ; end; theorem :: TOPS_1:4 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "R" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "R" ($#k3_subset_1 :::"`"::: ) ) -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: TOPS_1:5 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set (Var "S"))))) ; theorem :: TOPS_1:6 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "K")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "K")) ($#k7_subset_1 :::"\"::: ) (Set (Var "L")) ")" ))))) ; theorem :: TOPS_1:7 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "S")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "R")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "S")) ")" ))))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); let "P", "Q" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TS")); cluster (Set "P" ($#k3_xboole_0 :::"/\"::: ) "Q") -> ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "TS"; cluster (Set "P" ($#k2_xboole_0 :::"\/"::: ) "Q") -> ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "TS"; end; theorem :: TOPS_1:8 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: TOPS_1:9 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); let "P", "Q" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TS")); cluster (Set "P" ($#k3_xboole_0 :::"/\"::: ) "Q") -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "TS"; cluster (Set "P" ($#k2_xboole_0 :::"\/"::: ) "Q") -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "TS"; end; theorem :: TOPS_1:10 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPS_1:11 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPS_1:12 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "R")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "T")))) ")" )))) ; theorem :: TOPS_1:13 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Q")) "," (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "K")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "K")) ")" ))))) ; theorem :: TOPS_1:14 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Q")) "," (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "K")) ")" ))))) ; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); func :::"Int"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" equals :: TOPS_1:def 1 (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" "R" ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ); projectivity (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "b2")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "b1")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ))) ; end; :: deftheorem defines :::"Int"::: TOPS_1:def 1 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )))); theorem :: TOPS_1:15 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "TS")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "TS"))))) ; theorem :: TOPS_1:16 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set (Var "T"))))) ; theorem :: TOPS_1:17 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "K")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "K")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "L")) ")" ))))) ; registrationlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) "GX" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: TOPS_1:18 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "GX")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "GX"))))) ; theorem :: TOPS_1:19 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Var "W")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "W")))))) ; theorem :: TOPS_1:20 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "T")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "W")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "W")) ")" ))))) ; theorem :: TOPS_1:21 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "K")) ($#k7_subset_1 :::"\"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "K")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "L")) ")" ))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "K" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k1_tops_1 :::"Int"::: ) "K") -> ($#v3_pre_topc :::"open"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); cluster (Set ($#k2_struct_0 :::"[#]"::: ) "T") -> ($#v3_pre_topc :::"open"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))); end; theorem :: TOPS_1:22 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "K")))) "iff" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "K"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) ")" )) ")" )))) ; theorem :: TOPS_1:23 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) )) "implies" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) ")" & "(" (Bool (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "P")))) "implies" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ")" ))))) ; theorem :: TOPS_1:24 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "T")))))) ; theorem :: TOPS_1:25 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) "iff" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) ")" )) ")" )) ")" ))) ; theorem :: TOPS_1:26 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "T")) ")" ) ")" ) ")" ))))) ; theorem :: TOPS_1:27 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")))))) ; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); func :::"Fr"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" equals :: TOPS_1:def 2 (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) "R" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" "R" ($#k3_subset_1 :::"`"::: ) ")" ) ")" )); end; :: deftheorem defines :::"Fr"::: TOPS_1:def 2 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))); registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "A") -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: TOPS_1:28 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S"))) ")" )) ")" )))) ; theorem :: TOPS_1:29 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" (Set (Var "T")) ($#k3_subset_1 :::"`"::: ) ")" ))))) ; theorem :: TOPS_1:30 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "T")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "T")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "T")) ")" ))))) ; theorem :: TOPS_1:31 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")) ")" ))))) ; theorem :: TOPS_1:32 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" (Set (Var "K")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "K")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "L")) ")" ))))) ; theorem :: TOPS_1:33 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" (Set (Var "K")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "K")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "L")) ")" ))))) ; theorem :: TOPS_1:34 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")))))) ; theorem :: TOPS_1:35 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "R"))))) ; theorem :: TOPS_1:36 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "K")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set "(" (Set (Var "K")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "L")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set "(" (Set (Var "K")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "L")) ")" ) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "K")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "L")) ")" ) ")" ))))) ; theorem :: TOPS_1:37 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "T")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")))))) ; theorem :: TOPS_1:38 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "T")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")))))) ; theorem :: TOPS_1:39 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "T"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")))))) ; theorem :: TOPS_1:40 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "T")) ")" ))))) ; theorem :: TOPS_1:41 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "K")) ")" ))))) ; theorem :: TOPS_1:42 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P")))) ")" ))) ; theorem :: TOPS_1:43 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "P")) ")" ))) ")" ))) ; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); attr "R" is :::"dense"::: means :: TOPS_1:def 3 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) "R") ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "GX")); end; :: deftheorem defines :::"dense"::: TOPS_1:def 3 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "GX")))) ")" ))); registrationlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "GX") -> ($#v1_tops_1 :::"dense"::: ) ; cluster ($#v1_tops_1 :::"dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "GX"))); end; theorem :: TOPS_1:44 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "S")) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; theorem :: TOPS_1:45 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_tops_1 :::"dense"::: ) ) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "P")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Q")))) ")" ))) ; theorem :: TOPS_1:46 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_tops_1 :::"dense"::: ) )) "holds" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P")) ")" )))))) ; theorem :: TOPS_1:47 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_tops_1 :::"dense"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q"))) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); attr "R" is :::"boundary"::: means :: TOPS_1:def 4 (Bool (Set "R" ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ); end; :: deftheorem defines :::"boundary"::: TOPS_1:def 4 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ) ")" ))); registrationlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_tops_1 :::"boundary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "GX"))); end; theorem :: TOPS_1:48 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; registrationlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v2_tops_1 :::"boundary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "GX"))); end; registrationlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#v2_tops_1 :::"boundary"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); cluster (Set ($#k1_tops_1 :::"Int"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: TOPS_1:49 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v2_tops_1 :::"boundary"::: ) ))) ; theorem :: TOPS_1:50 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))) ; theorem :: TOPS_1:51 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G"))) ")" ))) ")" ))) ; theorem :: TOPS_1:52 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_tops_1 :::"boundary"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R")))) ")" ))) ; registrationlet "GX" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_struct_0 :::"[#]"::: ) "GX") -> ($#~v2_tops_1 "non" ($#v2_tops_1 :::"boundary"::: ) ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v2_tops_1 "non" ($#v2_tops_1 :::"boundary"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "GX"))); end; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); attr "R" is :::"nowhere_dense"::: means :: TOPS_1:def 5 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) "R") "is" ($#v2_tops_1 :::"boundary"::: ) ); end; :: deftheorem defines :::"nowhere_dense"::: TOPS_1:def 5 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R"))) "is" ($#v2_tops_1 :::"boundary"::: ) ) ")" ))); registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_tops_1 :::"nowhere_dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS"))); end; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_tops_1 :::"nowhere_dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS"))); end; theorem :: TOPS_1:53 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; theorem :: TOPS_1:54 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); let "R" be ($#v3_tops_1 :::"nowhere_dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TS")); cluster (Set "R" ($#k3_subset_1 :::"`"::: ) ) -> ($#v1_tops_1 :::"dense"::: ) ; end; theorem :: TOPS_1:55 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v2_tops_1 :::"boundary"::: ) ))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_tops_1 :::"nowhere_dense"::: ) -> ($#v2_tops_1 :::"boundary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS"))); end; theorem :: TOPS_1:56 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v2_tops_1 :::"boundary"::: ) ) & (Bool (Set (Var "S")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_pre_topc :::"closed"::: ) ($#v2_tops_1 :::"boundary"::: ) -> ($#v3_tops_1 :::"nowhere_dense"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS"))); end; theorem :: TOPS_1:57 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R")))) ")" ))) ; theorem :: TOPS_1:58 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "P"))) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); let "P" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TS")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "P") -> ($#v3_tops_1 :::"nowhere_dense"::: ) ; end; theorem :: TOPS_1:59 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "P"))) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); let "P" be ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TS")); cluster (Set ($#k2_tops_1 :::"Fr"::: ) "P") -> ($#v3_tops_1 :::"nowhere_dense"::: ) ; end; theorem :: TOPS_1:60 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "P")) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) )) "holds" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; registrationlet "TS" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_pre_topc :::"open"::: ) ($#v3_tops_1 :::"nowhere_dense"::: ) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "TS"))); end; definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "R" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); attr "R" is :::"condensed"::: means :: TOPS_1:def 6 (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "R" ")" )) ($#r1_tarski :::"c="::: ) "R") & (Bool "R" ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "R" ")" ))) ")" ); attr "R" is :::"closed_condensed"::: means :: TOPS_1:def 7 (Bool "R" ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "R" ")" ))); attr "R" is :::"open_condensed"::: means :: TOPS_1:def 8 (Bool "R" ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "R" ")" ))); end; :: deftheorem defines :::"condensed"::: TOPS_1:def 6 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "R")) ")" ))) ")" ) ")" ))); :: deftheorem defines :::"closed_condensed"::: TOPS_1:def 7 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "R")) ")" ))) ")" ))); :: deftheorem defines :::"open_condensed"::: TOPS_1:def 8 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" ))) ")" ))); theorem :: TOPS_1:61 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) ")" ))) ; theorem :: TOPS_1:62 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) )) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R")))))) ; theorem :: TOPS_1:63 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) )) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "R")) ")" ))))) ; theorem :: TOPS_1:64 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v6_tops_1 :::"open_condensed"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" ))) & (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "R")))) ")" ))) ; theorem :: TOPS_1:65 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) "iff" (Bool (Set (Var "R")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) ")" ))) ; theorem :: TOPS_1:66 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "R")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "implies" (Bool (Set (Var "R")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "P")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) )) "implies" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "P")) "is" ($#v4_tops_1 :::"condensed"::: ) ) ")" ) ")" ")" ))))) ; theorem :: TOPS_1:67 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "implies" (Bool (Set (Var "R")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "P")) "is" ($#v6_tops_1 :::"open_condensed"::: ) )) "implies" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "P")) "is" ($#v4_tops_1 :::"condensed"::: ) ) ")" ) ")" ")" ))))) ; theorem :: TOPS_1:68 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v5_tops_1 :::"closed_condensed"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v5_tops_1 :::"closed_condensed"::: ) ))) ; theorem :: TOPS_1:69 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v6_tops_1 :::"open_condensed"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v6_tops_1 :::"open_condensed"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Q"))) "is" ($#v6_tops_1 :::"open_condensed"::: ) ))) ; theorem :: TOPS_1:70 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPS_1:71 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_tops_1 :::"condensed"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "R"))) "is" ($#v4_tops_1 :::"condensed"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "R"))) "is" ($#v4_tops_1 :::"condensed"::: ) ) ")" ))) ;