for n being Nat
for M being non empty TopSpace holds
( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )