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

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

end;

hence ( TOP-REAL n is without_boundary & TOP-REAL n is n -locally_euclidean ) by Def4; :: thesis: verum