now :: thesis: for p being Point of (TOP-REAL n) ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

hence
( TOP-REAL n is without_boundary & TOP-REAL n is n -locally_euclidean )
by Def4; :: thesis: verumlet 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

end;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