:: JORDAN2B  semantic presentation begin  


































registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   -> (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )); 
end; 
theorem :: JORDAN2B:1 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "st"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))))))) ; 
 
theorem :: JORDAN2B:2 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: JORDAN2B:3 (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 "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))))))) ; 
 
theorem :: JORDAN2B:4 (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")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "p")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))))) ; 
 
theorem :: JORDAN2B:5 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))))) ; 
 
theorem :: JORDAN2B:6 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "p2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))))) ; 
 
theorem :: JORDAN2B:7 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "n")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "i"))))) ; 
 
theorem :: JORDAN2B:8 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "n")) ")" )  ($#k2_rfinseq :::"/^"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )))) ; 
 
theorem :: JORDAN2B:9 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: JORDAN2B:10 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "n")) ")" )  ($#k3_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "r"))))) ; 
 
theorem :: JORDAN2B:11 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k1_euclid :::"REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )) & (Bool (Set (Set  "(" (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  ))  ")" ))))) ; 
 begin  
theorem :: JORDAN2B:12 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))))  "}"  ) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))))) ; 
 
theorem :: JORDAN2B:13 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set (Var "s1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))))  "}"  ) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))))) ; 
 
theorem :: JORDAN2B:14 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" )  "}"  ) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))))) ; 
 
theorem :: JORDAN2B:15 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" )  "}"  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" )  "}"  ))))) ; 
 
theorem :: JORDAN2B:16 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "u")) "," (Set (Var "r")) ")" ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set (Var "P"))) "is"   ($#v3_pre_topc :::"open"::: )  )))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 
theorem :: JORDAN2B:17 (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  (Bool  "for" (Set (Var "r")) "," (Set (Var "u1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "u1"))  ($#r1_hidden :::"="::: )  (Set (Var "u")))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "u")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set (Var "u1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "u1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r"))))  ")" )  "}"  ))) ; 
 
theorem :: JORDAN2B:18 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 begin  
theorem :: JORDAN2B:19 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k3_euclid :::"abs"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "s")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: JORDAN2B:20 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 1) ")" ) (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 notationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym :::"|[":::"r":::"]|"::: for :::"<*":::"r":::"*>":::; end; definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"|["::: redefine func :::"|[":::"r":::"]|"::: ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 1) ")" ); end; 
theorem :: JORDAN2B:21 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_rlvect_1 :::"*"::: )  (Set  ($#k1_jordan2b :::"|["::: ) (Set (Var "r")) ($#k1_jordan2b :::"]|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_jordan2b :::"|["::: ) (Set  "(" (Set (Var "s"))  ($#k8_real_1 :::"*"::: )  (Set (Var "r")) ")" ) ($#k1_jordan2b :::"]|"::: ) )))) ; 
 
theorem :: JORDAN2B:22 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k1_jordan2b :::"|["::: ) (Set  "(" (Set (Var "r1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r2")) ")" ) ($#k1_jordan2b :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_jordan2b :::"|["::: ) (Set (Var "r1")) ($#k1_jordan2b :::"]|"::: ) )  ($#k3_rlvect_1 :::"+"::: )  (Set  ($#k1_jordan2b :::"|["::: ) (Set (Var "r2")) ($#k1_jordan2b :::"]|"::: ) )))) ; 
 
theorem :: JORDAN2B:23 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k1_jordan2b :::"|["::: ) (Set (Var "r1")) ($#k1_jordan2b :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_jordan2b :::"|["::: ) (Set (Var "r2")) ($#k1_jordan2b :::"]|"::: ) ))) "holds"  (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set (Var "r2")))) ; 
 
theorem :: JORDAN2B:24 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))) ; 
 
theorem :: JORDAN2B:25 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))) ; 
 
theorem :: JORDAN2B:26 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" )  "}"  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))) ; 
 
theorem :: JORDAN2B:27 (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 1) ")" )  (Bool  "for" (Set (Var "r")) "," (Set (Var "u1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "u1")) ($#k9_finseq_1 :::"*>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "u")))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "u")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set (Var "u1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "u1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r"))))  ")" )  "}"  ))) ; 
 
theorem :: JORDAN2B:28 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 1) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 1) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Num 1)))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) ; 
 
theorem :: JORDAN2B:29 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  ))  ")" )) ; 
 
theorem :: JORDAN2B:30 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_pscomp_1 :::"proj1"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))) & (Bool (Set (Set (Var "p"))  ($#k7_partfun1 :::"/."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_pscomp_1 :::"proj2"::: ) )  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))  ")" )) ;