let n be natural number ; :: thesis: for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )
let M be non empty TopSpace; :: thesis: ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )

hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) implies M is n -locally_euclidean )

assume A1: M is n -locally_euclidean ; :: thesis: for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic
let p be Point of M; :: thesis: ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic
consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that
A2: U,B are_homeomorphic by A1, Lm1;
reconsider B = B as ball Subset of (TOP-REAL n) ;
take U = U; :: thesis: ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic
take B = B; :: thesis: U,B are_homeomorphic
thus U,B are_homeomorphic by A2; :: thesis: verum

end;

assume A3: for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ; :: thesis: M is n -locally_euclidean

now

let p be Point of M; :: thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
consider U being a_neighborhood of p, B being ball Subset of (TOP-REAL n) such that
A4: U,B are_homeomorphic by A3;
reconsider S = B as open Subset of (TOP-REAL n) ;
take U = U; :: thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S = S; :: thesis: U,S are_homeomorphic
thus U,S are_homeomorphic by A4; :: thesis: verum

end;

hence M is n -locally_euclidean by Def4; :: thesis: verum