:: deftheorem Def3 defines -locally_euclidean MFOLD_0:def 3 :
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 st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic );