theorem :: MFOLD_0:16

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