let M be non empty TopSpace; :: thesis: ( M is n -locally_euclidean implies M is locally_euclidean )
assume A1: M is n -locally_euclidean ; :: thesis: M is locally_euclidean
let p be Point of M; :: according to MFOLD_0:def 2 :: thesis: ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A1;
hence ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ; :: thesis: verum