theorem :: MFOLD_0:15
for M being non empty compact locally_euclidean TopSpace ex P being a_partition of the carrier of M st
for A being Subset of M st A in P holds
( A is open & A is a_component & ex n being Nat st M | A is non empty b4 -locally_euclidean TopSpace )