:: TOPS_2 semantic presentation begin theorem :: TOPS_2:1 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ))))) ; theorem :: TOPS_2:2 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")))))) ; theorem :: TOPS_2:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T")))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: TOPS_2:4 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "F")) ($#k7_subset_1 :::"\"::: ) (Set (Var "G")) ")" ))))) ; theorem :: TOPS_2:5 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: TOPS_2:6 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: TOPS_2:7 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F")) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: TOPS_2:8 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "iff" (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is :::"open"::: means :: TOPS_2:def 1 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )); attr "F" is :::"closed"::: means :: TOPS_2:def 2 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) )); end; :: deftheorem defines :::"open"::: TOPS_2:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))); :: deftheorem defines :::"closed"::: TOPS_2:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))); theorem :: TOPS_2:9 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) "iff" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) "is" ($#v1_tops_2 :::"open"::: ) ) ")" ))) ; theorem :: TOPS_2:10 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) "iff" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) "is" ($#v2_tops_2 :::"closed"::: ) ) ")" ))) ; theorem :: TOPS_2:11 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ))) ; theorem :: TOPS_2:12 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ))) ; theorem :: TOPS_2:13 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "G"))) "is" ($#v1_tops_2 :::"open"::: ) ))) ; theorem :: TOPS_2:14 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "G"))) "is" ($#v1_tops_2 :::"open"::: ) ))) ; theorem :: TOPS_2:15 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_subset_1 :::"\"::: ) (Set (Var "G"))) "is" ($#v1_tops_2 :::"open"::: ) ))) ; theorem :: TOPS_2:16 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "G"))) "is" ($#v2_tops_2 :::"closed"::: ) ))) ; theorem :: TOPS_2:17 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "G"))) "is" ($#v2_tops_2 :::"closed"::: ) ))) ; theorem :: TOPS_2:18 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_subset_1 :::"\"::: ) (Set (Var "G"))) "is" ($#v2_tops_2 :::"closed"::: ) ))) ; theorem :: TOPS_2:19 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "W"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPS_2:20 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "W")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "W"))) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPS_2:21 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v2_tops_2 :::"closed"::: ) ) & (Bool (Set (Var "W")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "W"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: TOPS_2:22 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "W"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: TOPS_2:23 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "F")) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")))))) ; theorem :: TOPS_2:24 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )) ")" )))) ; theorem :: TOPS_2:25 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))))) ; theorem :: TOPS_2:26 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; theorem :: TOPS_2:27 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "G")) "is" ($#v1_tops_2 :::"open"::: ) ))))) ; theorem :: TOPS_2:28 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "G")) "is" ($#v2_tops_2 :::"closed"::: ) ))))) ; theorem :: TOPS_2:29 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "N")) ")" )))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "F" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); func "F" :::"|"::: "P" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" "T" ($#k1_pre_topc :::"|"::: ) "P" ")" ) means :: TOPS_2:def 3 (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "T" ($#k1_pre_topc :::"|"::: ) "P" ")" ) "holds" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Set (Var "R")) ($#k9_subset_1 :::"/\"::: ) "P") ($#r1_hidden :::"="::: ) (Set (Var "Q"))) ")" )) ")" )); end; :: deftheorem defines :::"|"::: TOPS_2:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "holds" (Bool "(" (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "R")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "R")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) ")" )) ")" )) ")" ))))); theorem :: TOPS_2:30 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M"))))))) ; theorem :: TOPS_2:31 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Q")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "M"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M"))))))) ; theorem :: TOPS_2:32 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Q")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M")) ")" )))))) ; theorem :: TOPS_2:33 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M")) ")" )))))) ; theorem :: TOPS_2:34 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))))))) ; theorem :: TOPS_2:35 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set (Var "M")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))))))) ; theorem :: TOPS_2:36 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M"))) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: TOPS_2:37 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M"))) "is" ($#v1_tops_2 :::"open"::: ) )))) ; theorem :: TOPS_2:38 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "M"))) "is" ($#v2_tops_2 :::"closed"::: ) )))) ; theorem :: TOPS_2:39 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool "(" "for" (Set (Var "AA")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "AA")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_tops_2 :::"|"::: ) (Set (Var "AA")))) ")" ) ")" ))))) ; theorem :: TOPS_2:40 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_tops_2 :::"|"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P"))))) ")" ) ")" ))))) ; theorem :: TOPS_2:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))))) ; theorem :: TOPS_2:42 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k3_funct_3 :::"""::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H"))) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))))))) ; theorem :: TOPS_2:43 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))) ; theorem :: TOPS_2:44 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P1")) ")" )))) ")" ))) ; theorem :: TOPS_2:45 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" )))) ")" )))) ; theorem :: TOPS_2:46 (Bool "for" (Set (Var "T")) "," (Set (Var "V")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))))) ; theorem :: TOPS_2:47 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "H")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_funct_3 :::"""::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )))))) ; theorem :: TOPS_2:48 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "H")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_funct_3 :::"""::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ))))) ; definitionlet "S", "T" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); assume (Bool (Set (Const "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) ; func "f" :::"/""::: -> ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" equals :: TOPS_2:def 4 (Set "f" ($#k2_funct_1 :::"""::: ) ); end; :: deftheorem defines :::"/""::: TOPS_2:def 4 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"/""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) )))); notationlet "S", "T" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); synonym "f" :::"""::: for "f" :::"/""::: ; end; theorem :: TOPS_2:49 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) ")" )))) ; theorem :: TOPS_2:50 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: TOPS_2:51 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Var "f")))))) ; theorem :: TOPS_2:52 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: TOPS_2:53 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")))) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k2_tops_2 :::"""::: ) ")" ))))))) ; theorem :: TOPS_2:54 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "P"))))))) ; theorem :: TOPS_2:55 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "P1"))))))) ; definitionlet "S", "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"being_homeomorphism"::: means :: TOPS_2:def 5 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "S")) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "T")) & (Bool "f" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "f" "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set "f" ($#k2_tops_2 :::"""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ); end; :: deftheorem defines :::"being_homeomorphism"::: TOPS_2:def 5 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ) ")" ))); theorem :: TOPS_2:56 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )))) ; theorem :: TOPS_2:57 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "," (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) )))) ; theorem :: TOPS_2:58 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: TOPS_2:59 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P1")) ")" ))) ")" ) ")" ) ")" )))) ; theorem :: TOPS_2:60 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))) ")" ) ")" ) ")" )))) ; theorem :: TOPS_2:61 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: TOPS_2:62 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; begin theorem :: TOPS_2:63 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) (Bool "ex" (Set (Var "GY")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool "(" (Bool (Set (Var "GY")) "is" ($#v1_connsp_1 :::"connected"::: ) ) & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "GY")) "," (Set (Var "GX")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) ")" )) ")" )) ")" )) "holds" (Bool (Set (Var "GX")) "is" ($#v1_connsp_1 :::"connected"::: ) )) ; theorem :: TOPS_2:64 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) "iff" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) ")" ))) ; theorem :: TOPS_2:65 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) "iff" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))))) ")" ))) ; registrationlet "X" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "X") -> ($#v1_tops_2 :::"open"::: ) ; cluster ($#v1_tops_2 :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" )); end;