:: TOPREAL4 semantic presentation begin definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred "P" :::"is_S-P_arc_joining"::: "p" "," "q" means :: TOPREAL4:def 1 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool "P" ($#r1_hidden :::"="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool "p" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool "q" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"is_S-P_arc_joining"::: TOPREAL4:def 1 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); attr "P" is :::"being_special_polygon"::: means :: TOPREAL4:def 2 (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )(Bool "ex" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) & (Bool "P" ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2")))) ")" ))); end; :: deftheorem defines :::"being_special_polygon"::: TOPREAL4:def 2 : (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_topreal4 :::"being_special_polygon"::: ) ) "iff" (Bool "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )(Bool "ex" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Set (Var "P1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "P2")))) ")" ))) ")" )); definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "P" is :::"being_Region"::: means :: TOPREAL4:def 3 (Bool "(" (Bool "P" "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "P" "is" ($#v2_connsp_1 :::"connected"::: ) ) ")" ); end; :: deftheorem defines :::"being_Region"::: TOPREAL4: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")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v2_topreal4 :::"being_Region"::: ) ) "iff" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "P")) "is" ($#v2_connsp_1 :::"connected"::: ) ) ")" ) ")" ))); theorem :: TOPREAL4:1 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "P")) "is" ($#v5_topreal1 :::"being_S-P_arc"::: ) ))) ; theorem :: TOPREAL4:2 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "P")) ($#r1_topreal1 :::"is_an_arc_of"::: ) (Set (Var "p")) "," (Set (Var "q"))))) ; theorem :: TOPREAL4:3 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) ")" ))) ; theorem :: TOPREAL4:4 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))))) ; theorem :: TOPREAL4:5 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_topreal4 :::"being_special_polygon"::: ) )) "holds" (Bool (Set (Var "P")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) ; theorem :: TOPREAL4:6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "q")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: TOPREAL4:7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "q")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: TOPREAL4:8 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "q")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: TOPREAL4:9 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "q")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: TOPREAL4:10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) ")" ))))) ; theorem :: TOPREAL4:11 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Num 1) ")" )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "p")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 1) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "p")) ")" ")" ))) ")" ))) ; theorem :: TOPREAL4:12 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Num 1) ")" )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "p")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 1) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set (Var "p")) ")" ")" ))) ")" ))) ; theorem :: TOPREAL4:13 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set (Var "p")) ")" ")" ))) ")" )))) ; theorem :: TOPREAL4:14 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2)) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 1) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ")" ))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 2) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ")" ))) ")" )) ; theorem :: TOPREAL4:15 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2)) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 1) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ")" ))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 2) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ")" ))) ")" )) ; theorem :: TOPREAL4:16 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Num 2)) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i"))))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ")" ))) ")" ))) ; theorem :: TOPREAL4:17 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) "," (Set (Var "p")) ")" ")" ))) ")" ))))) ; theorem :: TOPREAL4:18 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))) ")" )))) ; theorem :: TOPREAL4:19 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) ")" ) ")" ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set (Var "p")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ")" ))) ")" ))))) ; theorem :: TOPREAL4:20 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "p")) ($#k2_finseq_4 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ")" ))) ")" ))))) ; theorem :: TOPREAL4:21 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "p")) ($#k2_finseq_4 :::"*>"::: ) ))) & (Bool (Set (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ")" ))) ")" ))))) ; theorem :: TOPREAL4:22 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Bool "not" (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "f")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "," (Set (Var "p"))) & (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ")" ))) ")" )))))) ; theorem :: TOPREAL4:23 (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "p1"))) & (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" )) & (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "R")))) "holds" (Bool "ex" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p1")) "," (Set (Var "p"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" ))))))) ; theorem :: TOPREAL4:24 (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_topreal4 :::"being_Region"::: ) ) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool "(" "for" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) "or" "not" (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" ) ")" ) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPREAL4:25 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_topreal4 :::"being_Region"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "P")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPREAL4:26 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))))) ; theorem :: TOPREAL4:27 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_topreal4 :::"being_Region"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))))) ; theorem :: TOPREAL4:28 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "R")) "," (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_topreal4 :::"being_Region"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) "or" (Bool "ex" (Set (Var "P1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P1")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "P1")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" )) ")" ) "}" )) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: TOPREAL4:29 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_topreal4 :::"being_Region"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "P")) ($#r1_topreal4 :::"is_S-P_arc_joining"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) ")" )))) ;