let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic
let p, q be Point of (TOP-REAL n); :: 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 TOPREAL9:16, TOPS_1:24;
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 TOPREAL9:16, TOPS_1:24;
then ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) ;
then consider h being Function of ((TOP-REAL n) | (cl_Ball (p,r))),((TOP-REAL n) | (cl_Ball (q,s))) such that
A4: ( h is being_homeomorphism & h .: (Fr (cl_Ball (p,r))) = Fr (cl_Ball (q,s)) ) by A2, BROUWER2:7;
A5: [#] ((TOP-REAL n) | (cl_Ball (q,s))) = cl_Ball (q,s) by PRE_TOPC:def 5;
A6: h .: (dom h) = rng h by RELAT_1:113
.= [#] ((TOP-REAL n) | (cl_Ball (q,s))) by FUNCT_2:def 3, A4 ;
A7: Fr (cl_Ball (p,r)) = Sphere (p,r) by BROUWER2:5;
A8: [#] ((TOP-REAL n) | (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 TOPREAL9:18, TOPREAL9:19;
A10: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by TOPREAL9:18, TOPREAL9:19;
reconsider Br = Ball (p,r) as Subset of ((TOP-REAL n) | (cl_Ball (p,r))) by A10, A8, XBOOLE_1:7;
reconsider Bs = Ball (q,s) as Subset of ((TOP-REAL n) | (cl_Ball (q,s))) by A9, A5, XBOOLE_1:7;
A12: dom h = [#] ((TOP-REAL n) | (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 TOPREAL9:18, TOPREAL9:19;
A14: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by TOPREAL9:18, TOPREAL9:19;
(dom h) \ (Sphere (p,r)) = Ball (p,r) by A12, A8, XBOOLE_1:88, A14;
then h .: Br = (h .: (dom h)) \ (Fr (cl_Ball (q,s))) by A4, FUNCT_1:64, A7
.= (cl_Ball (q,s)) \ (Sphere (q,s)) by BROUWER2:5, A6, A5
.= Bs by A13, XBOOLE_1:88 ;
then ((TOP-REAL n) | (cl_Ball (p,r))) | Br,((TOP-REAL n) | (cl_Ball (q,s))) | Bs are_homeomorphic by A4, METRIZTS:3, METRIZTS:def 1;
then (TOP-REAL n) | (Ball (p,r)),((TOP-REAL n) | (cl_Ball (q,s))) | Bs are_homeomorphic by PRE_TOPC:7, A8;
hence Tball (p,r), Tball (q,s) are_homeomorphic by PRE_TOPC:7, A5; :: thesis: verum