:: deftheorem Def4 defines Int MFOLD_0:def 4 :
for M being non empty TopSpace
for b₂ being Subset of M holds
( b₂ = Int M iff for p being Point of M holds
( p in b₂ iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) );