:: TOPREAL6  semantic presentation begin  







































theorem :: TOPREAL6:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: TOPREAL6:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "b"))))) ; 
 
theorem :: TOPREAL6:3 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "b"))))) ; 
 
theorem :: TOPREAL6:4 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: TOPREAL6:5 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Num 1)  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) ; 
 
theorem :: TOPREAL6:6 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Num 2)  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set (Var "r"))))) ; 
 
theorem :: TOPREAL6:7 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "r")))))) ; 
 
theorem :: TOPREAL6:8 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "iff" (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "j"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: TOPREAL6:9 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool (Set   ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k21_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "j"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "r")) ")" ) ")" ))))) ; 
 
theorem :: TOPREAL6:10 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "j")) "," (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k2_newton :::"|^"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k2_newton :::"|^"::: )  (Set (Var "i")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "r"))  ($#k2_newton :::"|^"::: )  (Set (Var "j")) ")" ))))) ; 
 




theorem :: TOPREAL6:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k12_rvsum_1 :::"sqr"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "a"))  ($#k5_square_1 :::"^2"::: )  ")" ) "," (Set  "(" (Set (Var "b"))  ($#k5_square_1 :::"^2"::: )  ")" ) ($#k2_finseq_4 :::"*>"::: ) ))) ; 
 
theorem :: TOPREAL6:12 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k3_euclid :::"abs"::: )  (Set (Var "F")) ")" ))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i"))))) "holds"  (Bool (Set (Set  "("  ($#k3_euclid :::"abs"::: )  (Set (Var "F")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a"))))))) ; 
 
theorem :: TOPREAL6:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k3_euclid :::"abs"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" ) "," (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "b")) ")" ) ($#k2_finseq_4 :::"*>"::: ) ))) ; 
 
theorem :: TOPREAL6:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d")))) "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "d"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "d"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: TOPREAL6:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; 
 
theorem :: TOPREAL6:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; 
 
theorem :: TOPREAL6:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) ; 
 begin  registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "A" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "A") ->   ($#v8_struct_0 :::"finite"::: )   ; 
end; registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v2_connsp_1 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 
end; 
theorem :: TOPREAL6:18 canceled; 
 
theorem :: TOPREAL6:19 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v1_connsp_1 :::"connected"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_connsp_1 :::"connected"::: )  )) ; 
 
theorem :: TOPREAL6:20 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" )) "holds"  (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))) "is"   ($#v2_compts_1 :::"compact"::: )  ))) ; 
 begin  
theorem :: TOPREAL6:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "D")))) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "C")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "B")) "," (Set (Var "D")) ")"  ")" )))) ; 
 
theorem :: TOPREAL6:22 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) ; 
 
theorem :: TOPREAL6:23 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k19_euclid :::"]|"::: ) ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a")))) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a"))))  ")" )) ; 
 
theorem :: TOPREAL6:24 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) "holds"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: TOPREAL6:25 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_euclid :::"0.REAL"::: )  (Num 2))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "z")))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "z")) ($#k12_euclid :::".|"::: ) )))) ; 
 
theorem :: TOPREAL6:26 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" ) "," (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )))) ; 
 
theorem :: TOPREAL6:27 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "s")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))) ; 
 
theorem :: TOPREAL6:28 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "s")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)))) ; 
 
theorem :: TOPREAL6:29 (Bool  "for" (Set (Var "s")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p"))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "s"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ))  ")" )) ; 
 
theorem :: TOPREAL6:30 (Bool  "for" (Set (Var "s")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p"))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "s"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ))  ")" )) ; 
 
theorem :: TOPREAL6:31 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#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) ")" ) (Bool  "ex" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "D")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))  ")" )))) ; 
 
theorem :: TOPREAL6:32 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#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) ")" ) (Bool  "ex" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "D")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))  ")" )))) ; 
 
theorem :: TOPREAL6:33 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#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) ")" ) (Bool  "ex" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "D")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))  ")" )))) ; 
 
theorem :: TOPREAL6:34 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#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) ")" ) (Bool  "ex" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "D")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))  ")" )))) ; 
 registration
cluster  ($#~v1_sppol_1  "non"   ($#v1_sppol_1 :::"horizontal"::: )   )   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 

cluster  ($#~v2_sppol_1  "non"   ($#v2_sppol_1 :::"vertical"::: )   )   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 

cluster   ($#v2_topreal4 :::"being_Region"::: )    ->   ($#v3_pre_topc :::"open"::: )     ($#v2_connsp_1 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 

cluster   ($#v3_pre_topc :::"open"::: )     ($#v2_connsp_1 :::"connected"::: )    ->   ($#v2_topreal4 :::"being_Region"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 
end; registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_sppol_1 :::"horizontal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 

cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v2_sppol_1 :::"vertical"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_convex1 :::"convex"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); 
cluster (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" "a" "," "b" ")" ) ->   ($#v2_connsp_1 :::"connected"::: )   ; 
end; registration
cluster (Set   ($#k1_topreal1 :::"R^2-unit_square"::: )  ) ->   ($#v2_connsp_1 :::"connected"::: )   ; 
end; registration
cluster   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ->   ($#v2_connsp_1 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))); 
end; 
theorem :: TOPREAL6:35 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "("  ($#k12_pscomp_1 :::"NE-corner"::: )  (Set (Var "P")) ")" ) "," (Set  "("  ($#k13_pscomp_1 :::"SE-corner"::: )  (Set (Var "P")) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_sprect_1 :::"SpStSeq"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:36 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "("  ($#k10_pscomp_1 :::"SW-corner"::: )  (Set (Var "P")) ")" ) "," (Set  "("  ($#k13_pscomp_1 :::"SE-corner"::: )  (Set (Var "P")) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_sprect_1 :::"SpStSeq"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:37 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "("  ($#k10_pscomp_1 :::"SW-corner"::: )  (Set (Var "P")) ")" ) "," (Set  "("  ($#k11_pscomp_1 :::"NW-corner"::: )  (Set (Var "P")) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_sprect_1 :::"SpStSeq"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:38 (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) : (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "C"))))  "}"   "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_connsp_1 :::"connected"::: )     ($#v1_convex1 :::"convex"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) ; 
 begin  



theorem :: TOPREAL6:39 (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r"))))  ")" )))) ; 
 
theorem :: TOPREAL6:40 (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r"))))  ")" )))) ; 
 
theorem :: TOPREAL6:41 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" ) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ) "," (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" ) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k6_real_1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Num 2) ")" ) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))))) ; 
 
theorem :: TOPREAL6:42 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) "," (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")"  ")" )))))) ; 
 
theorem :: TOPREAL6:43 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (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"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) )))))) ; 
 
theorem :: TOPREAL6:44 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (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"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) )))))) ; 
 
theorem :: TOPREAL6:45 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))))))) ; 
 
theorem :: TOPREAL6:46 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set   ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")))))))) ; 
 
theorem :: TOPREAL6:47 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set   ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "r")))))))) ; 
 
theorem :: TOPREAL6:48 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "e")))) "holds"  (Bool (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "r")))))))) ; 
 
theorem :: TOPREAL6:49 (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds"  (Bool  "not" (Bool (Set (Var "D")) "is"   ($#v1_sppol_1 :::"horizontal"::: )  ))))) ; 
 
theorem :: TOPREAL6:50 (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds"  (Bool  "not" (Bool (Set (Var "D")) "is"   ($#v2_sppol_1 :::"vertical"::: )  ))))) ; 
 
theorem :: TOPREAL6:51 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ))) "holds"  (Bool  "not" (Bool (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) "," (Set  "(" (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  ")" ) ($#k19_euclid :::"]|"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" )))))) ; 
 
theorem :: TOPREAL6:52 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "X")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "X")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "X")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "X")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" ) ")" ))))) ; 
 
theorem :: TOPREAL6:53 (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"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k11_metric_1 :::"Sphere"::: )   "(" (Set (Var "z")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))))) ; 
 
theorem :: TOPREAL6:54 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v7_metric_1 :::"discerning"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k11_metric_1 :::"Sphere"::: )   "(" (Set (Var "z")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: TOPREAL6:55 (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"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "z")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))))) ; 
 
theorem :: TOPREAL6:56 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "z")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: TOPREAL6:57 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "z")) "," (Set (Var "r")) ")" ))) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ))))) ; 
 
theorem :: TOPREAL6:58 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "w")) "," (Set (Var "r")) ")" ))) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ))))) ; 
 
theorem :: TOPREAL6:59 (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"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )))) ; 
 
theorem :: TOPREAL6:60 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_metric_1 :::"Sphere"::: )   "(" (Set (Var "z")) "," (Set (Var "r")) ")" ))) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ))))) ; 
 
theorem :: TOPREAL6:61 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_metric_1 :::"Sphere"::: )   "(" (Set (Var "w")) "," (Set (Var "r")) ")" ))) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ))))) ; 
 
theorem :: TOPREAL6:62 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k11_metric_1 :::"Sphere"::: )   "(" (Set (Var "z")) "," (Set (Var "r")) ")" ) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )))) ; 
 
theorem :: TOPREAL6:63 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A"))) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ))) ; 
 
theorem :: TOPREAL6:64 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v5_tbsp_1 :::"bounded"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds"  (Bool (Set (Var "X")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ))  ")" )) ; 
 
theorem :: TOPREAL6:65 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")))) & (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v5_tbsp_1 :::"bounded"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "Y")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )))) ; 
 
theorem :: TOPREAL6:66 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")))) & (Bool (Set (Var "X")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "Y")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )))) ; 
 
theorem :: TOPREAL6:67 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ))) ; 
 begin  registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k6_measure6 :::"Cl"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "D" be   ($#v3_xxreal_2 :::"bounded_below"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k6_measure6 :::"Cl"::: )  "D") ->   ($#v3_xxreal_2 :::"bounded_below"::: )   ; 
end; registrationlet "D" be   ($#v4_xxreal_2 :::"bounded_above"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k6_measure6 :::"Cl"::: )  "D") ->   ($#v4_xxreal_2 :::"bounded_above"::: )   ; 
end; 
theorem :: TOPREAL6:68 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_xxreal_2 :::"bounded_below"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "("  ($#k6_measure6 :::"Cl"::: )  (Set (Var "D")) ")" )))) ; 
 
theorem :: TOPREAL6:69 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_xxreal_2 :::"bounded_above"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k6_measure6 :::"Cl"::: )  (Set (Var "D")) ")" )))) ; 
 registration
cluster (Set   ($#k3_topmetr :::"R^1"::: )  ) ->   ($#v8_pre_topc :::"T_2"::: )   ; 
end; 
theorem :: TOPREAL6:70 canceled; 
 
theorem :: TOPREAL6:71 canceled; 
 
theorem :: TOPREAL6:72 canceled; 
 
theorem :: TOPREAL6:73 canceled; 
 
theorem :: TOPREAL6:74 canceled; 
 
theorem :: TOPREAL6:75 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" ))))) ; 
 
theorem :: TOPREAL6:76 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) ; 
 
theorem :: TOPREAL6:77 (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  ) ; 
 begin  
theorem :: TOPREAL6:78 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_rcomp_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )) "is"   ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ))) ; 
 
theorem :: TOPREAL6:79 (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"   ($#v9_rltopsp1 :::"bounded"::: )  ) & (Bool (Set (Var "P")) "is"   ($#v4_pre_topc :::"closed"::: )  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v2_compts_1 :::"compact"::: )  )) ; 
 
theorem :: TOPREAL6:80 (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"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool  "for" (Set (Var "g")) "being"   ($#v1_pscomp_1 :::"continuous"::: )    ($#m1_subset_1 :::"RealMap":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set  "(" (Set (Var "g"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "g"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "P")) ")" ))))) ; 
 
theorem :: TOPREAL6:81 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "P")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_measure6 :::"Cl"::: )  (Set  "(" (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:82 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "P")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_measure6 :::"Cl"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:83 (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"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set  "(" (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:84 (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"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set  "(" (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "P")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "P")) ")" )))) ; 
 
theorem :: TOPREAL6:85 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "D")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "D")) ")" )))) ; 
 
theorem :: TOPREAL6:86 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "D")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "D")) ")" )))) ; 
 
theorem :: TOPREAL6:87 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "D")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_pscomp_1 :::"N-bound"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "D")) ")" )))) ; 
 
theorem :: TOPREAL6:88 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "D")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_pscomp_1 :::"S-bound"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "D")) ")" )))) ; 
 
theorem :: TOPREAL6:89 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ) "or" (Bool (Set (Var "B")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )  ")" )) "holds"  (Bool (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B"))) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ))) ; 
 
theorem :: TOPREAL6:90 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )) "holds"  (Bool  "not" (Bool (Set (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set (Var "B"))) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )))) ; 
 begin  definitionlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"dist":::  "(" "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: TOPREAL6:def 1 (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  "n" ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  "a") & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  "b") & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" )  "st" (Bool (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Const "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))  ")" ))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Const "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))  ")" ))))
 ; end; 







:: deftheorem    defines :::"dist"::: TOPREAL6:def 1 :  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))  ")" ))  ")" )))); 
 






theorem :: TOPREAL6:91 (Bool  "for" (Set (Var "r1")) "," (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "s2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r1")) "," (Set (Var "s1")) ($#k19_euclid :::"]|"::: ) )) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "r2")) "," (Set (Var "s2")) ($#k19_euclid :::"]|"::: ) ))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "u")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "r1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))))) ; 
 
theorem :: TOPREAL6:92 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k18_euclid :::"`2"::: )  ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: TOPREAL6:93 (Bool  "for" (Set (Var "n")) "being"    ($#m2_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   ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: TOPREAL6:94 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "q")) "," (Set (Var "r")) ")"  ")" ))))) ; 
 
theorem :: TOPREAL6:95 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y2"))) & (Bool (Set (Var "x1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "b"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "b"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y2")))) "holds"  (Bool (Set   ($#k1_topreal6 :::"dist"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "x2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "y1")) ")" ))))) ;