let n be Nat; :: thesis: for M being non empty TopSpace holds
( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic )

let M be non empty TopSpace; :: thesis: ( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic )
set TRn = TOP-REAL n;
hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic ) implies ( M is n -locally_euclidean & M is without_boundary ) )
assume A1: ( M is n -locally_euclidean & M is without_boundary ) ; :: thesis: for p being Point of M ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic
let p be Point of M; :: thesis: ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic
the carrier of M = Int M by ;
then consider U being a_neighborhood of p, m being Nat such that
A2: M | U, Tball ((0. ()),1) are_homeomorphic by MFOLD_0:def 4;
set TR = TOP-REAL m;
consider W being a_neighborhood of p such that
A3: M | W, Tdisk ((0. ()),1) are_homeomorphic by ;
( p in Int U & p in Int W ) by CONNSP_2:def 1;
then n = m by ;
hence ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic by ; :: thesis: verum
end;
assume R: for p being Point of M ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic ; :: thesis: ( M is n -locally_euclidean & M is without_boundary )
K: for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. ()),1) are_homeomorphic
proof
let p be Point of M; :: thesis: ex U being a_neighborhood of p st M | U, Tball ((0. ()),1) are_homeomorphic
consider U being a_neighborhood of p, B being non empty ball Subset of () such that
B1: U,B are_homeomorphic by R, Lm1;
take U ; :: thesis: M | U, Tball ((0. ()),1) are_homeomorphic
consider q being Point of (), r being Real such that
B2: B = Ball (q,r) by Def1;
B3: M | U,() | (Ball (q,r)) are_homeomorphic by ;
p in Int U by CONNSP_2:def 1;
then B4: ex W being Subset of M st
( W is open & W c= U & p in W ) by TOPS_1:22;
r > 0 by B2;
then Tball (q,r), Tball ((0. ()),1) are_homeomorphic by MFOLD_0:3;
hence M | U, Tball ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
ZZ: now :: thesis: for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. ()),1) are_homeomorphic
let p be Point of M; :: thesis: ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. ()),1) are_homeomorphic
ex U being a_neighborhood of p st M | U, Tball ((0. ()),1) are_homeomorphic by K;
hence ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. ()),1) are_homeomorphic ; :: thesis: verum
end;
then F: ( M is without_boundary & M is locally_euclidean ) by MFOLD_0:6;
for p being Point of M ex U being a_neighborhood of p st M | U, Tdisk ((0. ()),1) are_homeomorphic
proof
let p be Point of M; :: thesis: ex U being a_neighborhood of p st M | U, Tdisk ((0. ()),1) are_homeomorphic
consider U being a_neighborhood of p, m being Nat such that
B1: M | U, Tdisk ((0. ()),1) are_homeomorphic by ;
consider W being a_neighborhood of p such that
A3: M | W, Tball ((0. ()),1) are_homeomorphic by K;
( p in Int U & p in Int W ) by CONNSP_2:def 1;
then n = m by ;
hence ex U being a_neighborhood of p st M | U, Tdisk ((0. ()),1) are_homeomorphic by B1; :: thesis: verum
end;
hence ( M is n -locally_euclidean & M is without_boundary ) by ; :: thesis: verum