let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r, s being real number st r > 0 & s > 0 holds
Tdisk (p,r), Tdisk (q,s) are_homeomorphic
set TR = TOP-REAL n;
let p, q be Point of (TOP-REAL n); :: thesis: for r, s being real number st r > 0 & s > 0 holds
Tdisk (p,r), Tdisk (q,s) are_homeomorphic
let r, s be real number ; :: thesis: ( r > 0 & s > 0 implies Tdisk (p,r), Tdisk (q,s) are_homeomorphic )
assume that
A1: r > 0 and
A2: s > 0 ; :: thesis: Tdisk (p,r), Tdisk (q,s) are_homeomorphic
Ball (q,s) c= Int (cl_Ball (q,s)) by TOPREAL9:16, TOPS_1:24;
then A3: ( not cl_Ball (q,s) is boundary & cl_Ball (q,s) is compact ) by A2;
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 ) by A1;
then ex h being Function of ((TOP-REAL n) | (cl_Ball (p,r))),((TOP-REAL n) | (cl_Ball (q,s))) st
( h is being_homeomorphism & h .: (Fr (cl_Ball (p,r))) = Fr (cl_Ball (q,s)) ) by A3, BROUWER2:7;
hence Tdisk (p,r), Tdisk (q,s) are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum