for M being non empty compact locally_euclidean TopSpace st M is connected holds
ex n being Nat st M is n -locally_euclidean