for M being non empty locally_euclidean TopSpace
for p being Point of M holds
( p in Fr M iff ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )