:: TOPREAL9 semantic presentation begin theorem :: TOPREAL9:1 canceled; theorem :: TOPREAL9:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: TOPREAL9:3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "n")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k22_euclid :::"1.REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREAL9:4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" )))) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ) & "(" (Bool (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ) & "(" (Bool (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ")" ))))) ; theorem :: TOPREAL9:5 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" )))) ; theorem :: TOPREAL9:6 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set (Var "z2"))) & (Bool (Set (Var "z1")) ($#r2_hidden :::"in"::: ) (Set ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "z3")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z2")) ($#r2_hidden :::"in"::: ) (Set ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "z3")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Ball"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: TOPREAL9:def 1 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) "x" ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "r") "}" ; func :::"cl_Ball"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: TOPREAL9:def 2 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) "x" ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "r") "}" ; func :::"Sphere"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: TOPREAL9:def 3 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) "x" ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) "r") "}" ; end; :: deftheorem defines :::"Ball"::: TOPREAL9:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )))); :: deftheorem defines :::"cl_Ball"::: TOPREAL9:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) "}" )))); :: deftheorem defines :::"Sphere"::: TOPREAL9:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) : (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "}" )))); theorem :: TOPREAL9:7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: TOPREAL9:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )))) ; theorem :: TOPREAL9:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))) ; theorem :: TOPREAL9:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ; theorem :: TOPREAL9:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))))) ; theorem :: TOPREAL9:12 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: TOPREAL9:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )))))) ; theorem :: TOPREAL9:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )))))) ; theorem :: TOPREAL9:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool (Set ($#k11_metric_1 :::"Sphere"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )))))) ; theorem :: TOPREAL9:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: TOPREAL9:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: TOPREAL9:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: TOPREAL9:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_topreal9 :::"Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_topreal9 :::"Ball"::: ) "(" "x" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TOPREAL9:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: TOPREAL9:21 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" "x" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TOPREAL9:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: TOPREAL9:23 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: TOPREAL9:24 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "z")) "," (Set (Var "r")) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_topreal9 :::"Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v3_pre_topc :::"open"::: ) ; cluster (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v4_pre_topc :::"closed"::: ) ; cluster (Set ($#k3_topreal9 :::"Sphere"::: ) "(" "x" "," "r" ")" ) -> ($#v4_pre_topc :::"closed"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_topreal9 :::"Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v9_rltopsp1 :::"bounded"::: ) ; cluster (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v9_rltopsp1 :::"bounded"::: ) ; cluster (Set ($#k3_topreal9 :::"Sphere"::: ) "(" "x" "," "r" ")" ) -> ($#v9_rltopsp1 :::"bounded"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_topreal9 :::"Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v1_convex1 :::"convex"::: ) ; cluster (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" "x" "," "r" ")" ) -> ($#v1_convex1 :::"convex"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); attr "f" is :::"homogeneous"::: means :: TOPREAL9:def 4 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); end; :: deftheorem defines :::"homogeneous"::: TOPREAL9:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_topreal9 :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" ))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ")" )) -> ($#v13_vectsp_1 :::"additive"::: ) ($#v1_topreal9 :::"homogeneous"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster bbbadV1_RELAT_1() bbbadV1_FUNCT_1() bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))) ($#v5_pre_topc :::"continuous"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v1_topreal9 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )))))); end; registrationlet "a", "c" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_jgraph_2 :::"AffineMap"::: ) "(" "a" "," (Set ($#k6_numbers :::"0"::: ) ) "," "c" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ($#v1_topreal9 :::"homogeneous"::: ) ; end; theorem :: TOPREAL9:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#v13_vectsp_1 :::"additive"::: ) ($#v1_topreal9 :::"homogeneous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "is" ($#v1_convex1 :::"convex"::: ) )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"halfline"::: "(" "p" "," "q" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) equals :: TOPREAL9:def 5 "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "l")) ")" ) ($#k1_rlvect_1 :::"*"::: ) "p" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "l")) ($#k1_rlvect_1 :::"*"::: ) "q" ")" ) ")" ) where l "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) "}" ; end; :: deftheorem defines :::"halfline"::: TOPREAL9:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "l")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "l")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) where l "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) "}" ))); theorem :: TOPREAL9:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) "iff" (Bool "ex" (Set (Var "l")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "l")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "l")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) ")" )) ")" )))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k4_topreal9 :::"halfline"::: ) "(" "p" "," "q" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TOPREAL9:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; theorem :: TOPREAL9:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; theorem :: TOPREAL9:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: TOPREAL9:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; theorem :: TOPREAL9:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )))) ; theorem :: TOPREAL9:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k4_topreal9 :::"halfline"::: ) "(" "p" "," "q" ")" ) -> ($#v1_convex1 :::"convex"::: ) ; end; theorem :: TOPREAL9:33 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: TOPREAL9:34 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: TOPREAL9:35 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) ))))) ; theorem :: TOPREAL9:36 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) ))))) ; theorem :: TOPREAL9:37 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "X")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "S")) ($#k8_euclid :::"-"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) ")" )))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) ")" )))))) ; theorem :: TOPREAL9:38 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "Y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "e")) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ))) & "(" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) "implies" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "S")) ($#k8_euclid :::"-"::: ) (Set (Var "Y")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) ")" )))) "implies" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) ")" ")" )))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_topreal9 :::"Sphere"::: ) "(" "x" "," "r" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_topreal9 :::"Sphere"::: ) "(" "x" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TOPREAL9:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: TOPREAL9:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "n")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; begin theorem :: TOPREAL9:41 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))))) ; theorem :: TOPREAL9:42 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k18_euclid :::"`2"::: ) ")" ) ")" ))))) ; theorem :: TOPREAL9:43 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) ; theorem :: TOPREAL9:44 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ))) ; theorem :: TOPREAL9:45 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))) ; registrationlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" "a" "," "b" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" "a" "," "b" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: TOPREAL9:46 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:47 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ))) "holds" (Bool (Set ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )))) ; theorem :: TOPREAL9:48 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )))) ; theorem :: TOPREAL9:49 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ))) "holds" (Bool (Set ($#k11_metric_1 :::"Sphere"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )))) ; theorem :: TOPREAL9:50 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:51 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_topreal9 :::"cl_Ball"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:52 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:53 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:54 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:55 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) ; theorem :: TOPREAL9:56 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "s")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) )))) ; theorem :: TOPREAL9:57 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: TOPREAL9:58 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "w")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "X")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "s")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "s")) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "S")) ($#k8_euclid :::"-"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" ))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "w")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ))) ")" ))))) ; theorem :: TOPREAL9:59 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: TOPREAL9:60 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )))) ; theorem :: TOPREAL9:61 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: TOPREAL9:62 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Set "(" ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: TOPREAL9:63 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "w")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "Y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "t"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set (Var "s"))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "e")) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_topreal9 :::"halfline"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_jgraph_6 :::"circle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) ")" ")" ))) & "(" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ))) "implies" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) "," (Set (Var "r")) ")" ))) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "t")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) ) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "S")) ($#k8_euclid :::"-"::: ) (Set (Var "Y")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_euclid :::"sqr"::: ) (Set "(" (Set (Var "T")) ($#k8_euclid :::"-"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) ")" )))) "implies" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "w")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "t")) ")" ))) ")" ")" ))))) ; registrationlet "a", "b", "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k6_jgraph_6 :::"inside_of_circle"::: ) "(" "a" "," "b" "," "r" ")" ) -> ($#v1_convex1 :::"convex"::: ) ; cluster (Set ($#k7_jgraph_6 :::"closed_inside_of_circle"::: ) "(" "a" "," "b" "," "r" ")" ) -> ($#v1_convex1 :::"convex"::: ) ; end;