:: deftheorem defines Fr MFOLD_0:def 8 :
for n being Nat
for M being non empty b₁ -locally_euclidean TopSpace
for b₃ being Subset of M holds
( b₃ = Fr M iff for p being Point of M holds
( p in b₃ iff ex U being a_neighborhood of p 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) ) ) );