for n being Nat
for M1, M2 being non empty TopSpace st M1 is n -locally_euclidean & M2 is locally_euclidean & M1,M2 are_homeomorphic holds
M2 is n -locally_euclidean