:: deftheorem Def4 defines -locally_euclidean MFOLD_1:def 4 :
for n being Nat
for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic );