:: TOPGEN_5 semantic presentation begin theorem :: TOPGEN_5:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "g")) ($#k8_relat_1 :::"""::: ) (Set (Var "A")) ")" ))))) ; theorem :: TOPGEN_5:2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "g")) ($#k8_relat_1 :::"""::: ) (Set (Var "A")) ")" ))))) ; theorem :: TOPGEN_5:3 (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))))) ; theorem :: TOPGEN_5:4 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" ))) ")" ))) ; theorem :: TOPGEN_5:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" )) ")" ))) ; theorem :: TOPGEN_5:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))))) ; theorem :: TOPGEN_5:7 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "h")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ))))) ; theorem :: TOPGEN_5:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) )) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r2_tarski :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "X")) ")" ) ($#k2_card_2 :::"*`"::: ) (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "Y")) ")" ))) ")" )) ; scheme :: TOPGEN_5:sch 1 SCH1{ P1[ ($#m1_hidden :::"set"::: ) ], F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "a"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "a"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a")) ")" )) ")" ")" ))) provided (Bool (Set F3 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "a"))])) "implies" (Bool (Set F4 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "a"))])) "implies" (Bool (Set F5 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" ")" )) proof end; scheme :: TOPGEN_5:sch 2 SCH2{ P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "a"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "a"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "a")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "a"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "a")) ")" )) ")" ")" ))) provided (Bool (Set F3 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "a"))])) "implies" (Bool (Set F4 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "a"))])) "implies" (Bool (Set F5 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "a"))])) "implies" (Bool (Set F6 "(" (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" ")" )) proof end; theorem :: TOPGEN_5:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" )))) ; theorem :: TOPGEN_5:10 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) "," (Set (Var "Y")))))))) ; theorem :: TOPGEN_5:11 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) "," (Set (Var "Y")))))))) ; theorem :: TOPGEN_5:12 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")))))))) ; begin theorem :: TOPGEN_5:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ))))) ; definitionfunc :::"y=0-line"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: TOPGEN_5:def 1 "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool verum) "}" ; func :::"y>=0-plane"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: TOPGEN_5:def 2 "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ; end; :: deftheorem defines :::"y=0-line"::: TOPGEN_5:def 1 : (Bool (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool verum) "}" ); :: deftheorem defines :::"y>=0-plane"::: TOPGEN_5:def 2 : (Bool (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ); theorem :: TOPGEN_5:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: TOPGEN_5:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) "iff" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: TOPGEN_5:16 (Bool (Set ($#k1_card_1 :::"card"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_topgen_3 :::"continuum"::: ) )) ; theorem :: TOPGEN_5:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ) ")" )) ; theorem :: TOPGEN_5:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) "iff" (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; registration cluster (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TOPGEN_5:19 (Bool (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) ; theorem :: TOPGEN_5:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) "iff" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) ")" )) ; theorem :: TOPGEN_5:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) "iff" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) ")" )) ; theorem :: TOPGEN_5:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r2"))))) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "b")) "," (Set (Var "r2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "a")) "," (Set (Var "r1")) ")" ))))) ; theorem :: TOPGEN_5:23 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2")))) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "r1")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "r2")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r2")) ")" )))) ; theorem :: TOPGEN_5:24 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B1")) "being" ($#m1_topgen_2 :::"Neighborhood_System"::: ) "of" (Set (Var "T1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_topgen_2 :::"Neighborhood_System"::: ) "of" (Set (Var "T2")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))) "#)" ))))) ; definitionfunc :::"Niemytzki-plane"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) means :: TOPGEN_5:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) & (Bool "ex" (Set (Var "B")) "being" ($#m1_topgen_2 :::"Neighborhood_System"::: ) "of" it "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) where r "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ")" ) where r "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"Niemytzki-plane"::: TOPGEN_5:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) & (Bool "ex" (Set (Var "B")) "being" ($#m1_topgen_2 :::"Neighborhood_System"::: ) "of" (Set (Var "b1")) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" ) where r "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ")" ) where r "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ) ")" ) ")" )) ")" ) ")" )); theorem :: TOPGEN_5:25 (Bool (Set (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:26 (Bool (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:27 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )))) ; theorem :: TOPGEN_5:28 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )))) ; theorem :: TOPGEN_5:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )))) ; theorem :: TOPGEN_5:30 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )(Bool "ex" (Set (Var "U")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "b")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) ")" ))))) ; theorem :: TOPGEN_5:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "w")) "," (Set (Var "v")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "w")) "," (Set (Var "v")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "w")) "," (Set (Var "v")) ($#k19_euclid :::"]|"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) ")" )))) ; theorem :: TOPGEN_5:32 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ) ")" )))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ))))) ; theorem :: TOPGEN_5:33 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ))))) ; theorem :: TOPGEN_5:34 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )))) ; theorem :: TOPGEN_5:35 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: TOPGEN_5:36 (Bool (Set (Set "(" (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) "is" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:37 (Bool (Set (Set "(" (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:38 (Bool (Set (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) "is" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:39 (Bool (Set (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) )) "is" ($#v2_topgen_1 :::"dense-in-itself"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:40 (Bool (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) "is" ($#v3_tops_1 :::"nowhere_dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) )) ; theorem :: TOPGEN_5:41 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_topgen_5 :::"y=0-line"::: ) ))) "holds" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; theorem :: TOPGEN_5:42 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_topgen_5 :::"y=0-line"::: ) ) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ))) ; theorem :: TOPGEN_5:43 (Bool (Set ($#k3_numbers :::"RAT"::: ) ) "is" ($#v1_tops_1 :::"dense"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) )) ; theorem :: TOPGEN_5:44 (Bool (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ) "is" ($#v7_topgen_1 :::"separable"::: ) ) ; theorem :: TOPGEN_5:45 (Bool (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "is" ($#v7_topgen_1 :::"separable"::: ) ) ; theorem :: TOPGEN_5:46 (Bool (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "is" ($#v7_pre_topc :::"T_1"::: ) ) ; theorem :: TOPGEN_5:47 (Bool (Bool "not" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "is" ($#v10_pre_topc :::"normal"::: ) )) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); attr "T" is :::"Tychonoff"::: means :: TOPGEN_5:def 4 (Bool "for" (Set (Var "A")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "T" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ")" )))); end; :: deftheorem defines :::"Tychonoff"::: TOPGEN_5:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_topgen_5 :::"Tychonoff"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ")" )))) ")" )); registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_topgen_5 :::"Tychonoff"::: ) -> ($#v9_pre_topc :::"regular"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v12_pre_topc :::"T_4"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topgen_5 :::"Tychonoff"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: TOPGEN_5:48 (Bool "for" (Set (Var "X")) "being" ($#v7_pre_topc :::"T_1"::: ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_topgen_5 :::"Tychonoff"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "V")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ")" )))))) ; theorem :: TOPGEN_5:49 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "R")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))))) ; theorem :: TOPGEN_5:50 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "R")) (Bool "ex" (Set (Var "h")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "R")) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))))) ; theorem :: TOPGEN_5:51 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "R"))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "R")) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "S"))))))))))) ; theorem :: TOPGEN_5:52 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_pre_topc :::"T_1"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "V")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_topgen_5 :::"Tychonoff"::: ) ))) ; theorem :: TOPGEN_5:53 (Bool (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ) "is" ($#v7_pre_topc :::"T_1"::: ) ) ; theorem :: TOPGEN_5:54 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; theorem :: TOPGEN_5:55 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; theorem :: TOPGEN_5:56 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; theorem :: TOPGEN_5:57 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_rcomp_1 :::".["::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ))) ; theorem :: TOPGEN_5:58 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "w")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "w")) ($#k3_rcomp_1 :::".["::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "w")) ($#k3_rcomp_1 :::".["::: ) )))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ))))) ; theorem :: TOPGEN_5:59 (Bool (Set ($#k2_topgen_3 :::"Sorgenfrey-line"::: ) ) "is" ($#v1_topgen_5 :::"Tychonoff"::: ) ) ; begin definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; func :::"+"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) means :: TOPGEN_5:def 5 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) "x" "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) "x") "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Bool "not" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "x" "," "r" ($#k19_euclid :::"]|"::: ) ) "," "r" ")" )))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "x" "," "r" ($#k19_euclid :::"]|"::: ) ) "," "r" ")" ))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) "x" "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) "r" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ))) ")" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"+"::: TOPGEN_5:def 5 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Bool "not" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" )))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ))) ")" ")" )) ")" ) ")" ) ")" )))); theorem :: TOPGEN_5:60 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ))))) ; theorem :: TOPGEN_5:61 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "y")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: TOPGEN_5:62 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: TOPGEN_5:63 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a")))))) ; theorem :: TOPGEN_5:64 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a")))))) ; theorem :: TOPGEN_5:65 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) ")" ))))) ; theorem :: TOPGEN_5:66 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ))))) ; theorem :: TOPGEN_5:67 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k3_rcomp_1 :::".["::: ) ))))) ; theorem :: TOPGEN_5:68 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: TOPGEN_5:69 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) ")" ))))) ; theorem :: TOPGEN_5:70 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set (Var "r1")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r1")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: TOPGEN_5:71 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool "{" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")) ")" ) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "S")))) ")" ) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "S")))))) ; theorem :: TOPGEN_5:72 (Bool "{" (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) where a, b "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ; theorem :: TOPGEN_5:73 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "U")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "U")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))) "holds" (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))))) ; theorem :: TOPGEN_5:74 (Bool (Set (Set "(" "{" (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k3_rcomp_1 :::".["::: ) ) where a "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ) where a "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) where a, b "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" ) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) )) ; theorem :: TOPGEN_5:75 (Bool "for" (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 "T")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) ")" ))) ; registrationlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_topgen_5 :::"+"::: ) "(" "x" "," "r" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPGEN_5:76 (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "U")) ($#k3_subset_1 :::"`"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "U")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ))) ")" ")" ) ")" ) ")" ))))) ; definitionlet "x", "y" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; func :::"+"::: "(" "x" "," "y" "," "r" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) means :: TOPGEN_5:def 6 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "x" "," "y" ($#k19_euclid :::"]|"::: ) ) "," "r" ")" )))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) "x" "," "y" ($#k19_euclid :::"]|"::: ) ) "," "r" ")" ))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) "x" "," "y" ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k10_real_1 :::"/"::: ) "r")) ")" ")" ))); end; :: deftheorem defines :::"+"::: TOPGEN_5:def 6 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" )))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" ")" ))) ")" )))); theorem :: TOPGEN_5:77 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) ")" ))))) ; theorem :: TOPGEN_5:78 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k3_rcomp_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )))))) ; theorem :: TOPGEN_5:79 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a")))) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) ")" ))))) ; theorem :: TOPGEN_5:80 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a")))) "holds" (Bool "(" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")))) & (Bool "ex" (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set (Var "r1")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r1")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k5_topgen_5 :::"+"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) ")" )) ")" ))))) ; registrationlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "y", "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k5_topgen_5 :::"+"::: ) "(" "x" "," "y" "," "r" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPGEN_5:81 (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_topgen_5 :::"y>=0-plane"::: ) )))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "U")) ($#k3_subset_1 :::"`"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" ")" ) ")" ) ")" ))))) ; theorem :: TOPGEN_5:82 (Bool (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "is" ($#v7_pre_topc :::"T_1"::: ) ) ; theorem :: TOPGEN_5:83 (Bool (Set ($#k3_topgen_5 :::"Niemytzki-plane"::: ) ) "is" ($#v1_topgen_5 :::"Tychonoff"::: ) ) ;