let n be Nat; :: thesis: for p, q being Point of ()
for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic

let p, q be Point of (); :: thesis: for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic
set TR = TOP-REAL n;
let r, s be positive Real; :: thesis: Tball (p,r), Tball (q,s) are_homeomorphic
Ball (q,s) c= Int (cl_Ball (q,s)) by ;
then A2: ( not cl_Ball (q,s) is boundary & cl_Ball (q,s) is compact ) ;
Ball (p,r) c= Int (cl_Ball (p,r)) by ;
then ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) ;
then consider h being Function of (() | (cl_Ball (p,r))),(() | (cl_Ball (q,s))) such that
A4: ( h is being_homeomorphism & h .: (Fr (cl_Ball (p,r))) = Fr (cl_Ball (q,s)) ) by ;
A5: [#] (() | (cl_Ball (q,s))) = cl_Ball (q,s) by PRE_TOPC:def 5;
A6: h .: (dom h) = rng h by RELAT_1:113
.= [#] (() | (cl_Ball (q,s))) by ;
A7: Fr (cl_Ball (p,r)) = Sphere (p,r) by BROUWER2:5;
A8: [#] (() | (cl_Ball (p,r))) = cl_Ball (p,r) by PRE_TOPC:def 5;
A9: ( (Ball (q,s)) \/ (Sphere (q,s)) = cl_Ball (q,s) & Ball (q,s) misses Sphere (q,s) ) by ;
A10: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by ;
reconsider Br = Ball (p,r) as Subset of (() | (cl_Ball (p,r))) by ;
reconsider Bs = Ball (q,s) as Subset of (() | (cl_Ball (q,s))) by ;
A12: dom h = [#] (() | (cl_Ball (p,r))) by FUNCT_2:def 1;
A13: ( (Ball (q,s)) \/ (Sphere (q,s)) = cl_Ball (q,s) & Ball (q,s) misses Sphere (q,s) ) by ;
A14: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by ;
(dom h) \ (Sphere (p,r)) = Ball (p,r) by ;
then h .: Br = (h .: (dom h)) \ (Fr (cl_Ball (q,s))) by
.= (cl_Ball (q,s)) \ (Sphere (q,s)) by
.= Bs by ;
then ((TOP-REAL n) | (cl_Ball (p,r))) | Br,(() | (cl_Ball (q,s))) | Bs are_homeomorphic by ;
then (TOP-REAL n) | (Ball (p,r)),(() | (cl_Ball (q,s))) | Bs are_homeomorphic by ;
hence Tball (p,r), Tball (q,s) are_homeomorphic by ; :: thesis: verum