set MF = M | (Fr M);
now 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));
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
;
verum end;
hence
M | (Fr M) is locally_euclidean
by Lm2; verum