theorem Th13: :: MFOLD_0:13

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