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. ()),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. ()),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. ()),1) are_homeomorphic ) implies M is non empty locally_euclidean without_boundary TopSpace )
proof
assume 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. ()),1) are_homeomorphic
hence 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 by 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. ()),1) are_homeomorphic ) implies M is non empty locally_euclidean without_boundary TopSpace ) by Lm2; :: thesis: verum