let p be Point of (TOP-REAL n); :: thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
p in [#] (TOP-REAL n) ;
then p in Int ([#] (TOP-REAL n)) by TOPS_1:15;
then reconsider U = [#] (TOP-REAL n) as a_neighborhood of p by CONNSP_2:def 1;
reconsider S = U as open Subset of (TOP-REAL n) ;
take U = U; :: thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S = S; :: thesis: U,S are_homeomorphic
thus U,S are_homeomorphic by METRIZTS:1; :: thesis: verum