theorem :: MFOLD_0:6

for M being non empty TopSpace holds
( M is non empty locally_euclidean without_boundary TopSpace iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) by Lm2;