for n being Nat
for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds
stereographic_projection (S,p) is being_homeomorphism