set I = { p where p is 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 } ;
{ p where p is 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 } c= the carrier of M

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is 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 } or x in the carrier of M )
assume x in { p where p is 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: x in the carrier of M
then ex q being Point of M st
( x = q & ex U being a_neighborhood of q ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ;
hence x in the carrier of M ; :: thesis: verum

end;

then reconsider I = { p where p is 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 } as Subset of M ;
take I ; :: thesis: for p being Point of M holds
( p in I iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
let p be Point of M; :: thesis: ( p in I iff ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )

hereby :: thesis: ( ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic implies p in I )

assume p in I ; :: thesis: ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
then ex q being Point of M st
( p = q & ex U being a_neighborhood of q ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) ;
hence ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ; :: thesis: verum

end;

thus ( ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic implies p in I ) ; :: thesis: verum