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

let M be non empty TopSpace; :: thesis: ( ( M is without_boundary & M is n -locally_euclidean ) iff for p being Point of M ex U being a_neighborhood of p st U, [#] () are_homeomorphic )
hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p st U, [#] () are_homeomorphic ) implies ( M is without_boundary & M is n -locally_euclidean ) )
assume ( M is without_boundary & M is n -locally_euclidean ) ; :: thesis: for p being Point of M ex U being a_neighborhood of p st U, [#] () are_homeomorphic
then AA: for p being Point of M ex U being a_neighborhood of p ex S being open Subset of () st U,S are_homeomorphic by Def4;
let p be Point of M; :: thesis: ex U being a_neighborhood of p st U, [#] () are_homeomorphic
consider U being a_neighborhood of p, B being non empty ball Subset of () such that
A2: U,B are_homeomorphic by ;
take U = U; :: thesis:
A3: (TOP-REAL n) | ([#] ()) = TopStruct(# the carrier of (), the topology of () #) by TSEP_1:93;
reconsider B1 = () | B as non empty TopSpace ;
M | U,B1 are_homeomorphic by ;
then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;
A4: U1,B1 are_homeomorphic by ;
B1, TopStruct(# the carrier of (), the topology of () #) are_homeomorphic by ;
hence U, [#] () are_homeomorphic by ; :: thesis: verum
end;
assume A6: for p being Point of M ex U being a_neighborhood of p st U, [#] () are_homeomorphic ; :: thesis: ( M is without_boundary & M is n -locally_euclidean )
now :: 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
consider U being a_neighborhood of p such that
A7: U, [#] () are_homeomorphic by A6;
set S = the non empty ball Subset of ();
reconsider S = the non empty ball Subset of () as open Subset of () ;
take U = U; :: thesis: ex S being open Subset of () st U,S are_homeomorphic
take S = S; :: thesis:
A9: (TOP-REAL n) | ([#] ()) = TopStruct(# the carrier of (), the topology of () #) by TSEP_1:93;
A10: M | U, TopStruct(# the carrier of (), the topology of () #) are_homeomorphic by ;
then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;
reconsider S1 = () | S as non empty TopSpace ;
A11: TopStruct(# the carrier of (), the topology of () #),S1 are_homeomorphic by ;
U1,S1 are_homeomorphic by ;
hence U,S are_homeomorphic by METRIZTS:def 1; :: thesis: verum
end;
hence ( M is without_boundary & M is n -locally_euclidean ) by Def4; :: thesis: verum