for n, m being Nat
for M being non empty TopSpace st M is n -locally_euclidean & M is m -locally_euclidean holds
n = m