set MF = M | (Fr M);
n > 0 ;
then reconsider n1 = n - 1 as Nat by NAT_1:20;
A1: [#] (M | (Fr M)) = Fr M by PRE_TOPC:def 5;

let pF be Point of (M | (Fr M)); :: thesis:
pF in [#] (M | (Fr M)) ;
then reconsider p = pF as Point of M by A1;
consider U being a_neighborhood of p such that
A3: M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;
M | U, Tdisk ((0. (TOP-REAL (n1 + 1))),1) are_homeomorphic by A3;
hence ex W being a_neighborhood of pF st (M | (Fr M)) | W, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic by Th7; :: thesis:

end;