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 )

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

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
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. (TOP-REAL n)),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. (TOP-REAL n)),1) are_homeomorphic by Lm2; :: thesis: verum

end;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 Lm2; :: thesis: verum