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;

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

let pF be Point of (M | (Fr M)); :: thesis: ex W being a_neighborhood of pF st (M | (Fr M)) | W, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic
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: verum

end;

n -' 1 = n1 by XREAL_0:def 2;
hence for b₁ being non empty TopSpace st b₁ = M | (Fr M) holds
b₁ is n -' 1 -locally_euclidean by A2, Th13; :: thesis: verum