theorem :: BROUWER3:19

for n being Nat
for p, q being Point of (TOP-REAL (n + 1))
for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds
ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )