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

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 )

{ 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

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 ;
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;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

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 )

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: verumassume
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;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