theorem Th13: :: MFOLD_1:13

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 U, [#] (TOP-REAL n) are_homeomorphic )