for p being Point of (M | (Int M)) ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by Lm4;
hence M | (Int M) is locally_euclidean by Lm2; :: thesis: verum