let M be non empty TopSpace; :: thesis: ( M is non empty locally_euclidean without_boundary TopSpace iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
thus ( M is non empty locally_euclidean without_boundary TopSpace implies for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) implies M is non empty locally_euclidean without_boundary TopSpace )

proof

assume A1: M is non empty locally_euclidean without_boundary TopSpace ; :: thesis: for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
then for M1 being non empty locally_euclidean TopSpace st M1 = M holds
M1 is without_boundary ;
hence for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1, Lm2; :: thesis: verum

end;

thus ( ( for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) implies M is non empty locally_euclidean without_boundary TopSpace ) by Lm2; :: thesis: verum