set MF = M | (Fr M);

now :: thesis: for pM being Point of (M | (Fr M)) ex U being a_neighborhood of pM ex n1 being Nat st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic

let pM be Point of (M | (Fr M)); :: thesis: ex U being a_neighborhood of pM ex n1 being Nat st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic
A1: [#] (M | (Fr M)) = Fr M by PRE_TOPC:def 5;
then pM in Fr M ;
then reconsider p = pM as Point of M ;
consider U being a_neighborhood of p, n being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) such that
A2: h is being_homeomorphism and
A3: h . p in Sphere ((0. (TOP-REAL n)),1) by Th5, A1;
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic ) by Lm5, A2, A3;
hence ex U being a_neighborhood of pM ex n1 being Nat st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic ; :: thesis: verum

end;

hence M | (Fr M) is locally_euclidean by Lm2; :: thesis: verum