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
A4: [#] (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
A5: h is being_homeomorphism and
A6: h . p in Sphere ((0. (TOP-REAL n)),1) by Th5, A4;
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, A5, A6;
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 without_boundary by Lm2; :: thesis: verum