{ p where p is Point of (TOP-REAL n) : |.(p - x).| < r } c= the carrier of (TOP-REAL n)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } or q in the carrier of (TOP-REAL n) )
assume q in { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ; :: thesis: q in the carrier of (TOP-REAL n)
then ex p being Point of (TOP-REAL n) st
( q = p & |.(p - x).| < r ) ;
hence q in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

hence { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } is Subset of (TOP-REAL n) ; :: thesis: verum