theorem Th4: :: BROUWER3:4

for n being Nat
for p being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n)
for r being Real st not p in A & r > 0 holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )