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 b₄ -locally_euclidean TopSpace )