let n be Element of NAT ; :: thesis: for r being real number
for y, x being Point of (TOP-REAL n) holds
( y in Ball x,r iff |.(y - x).| < r )
let r be real number ; :: thesis: for y, x being Point of (TOP-REAL n) holds
( y in Ball x,r iff |.(y - x).| < r )
let y, x be Point of (TOP-REAL n); :: thesis: ( y in Ball x,r iff |.(y - x).| < r )

hereby :: thesis: ( |.(y - x).| < r implies y in Ball x,r )

assume y in Ball x,r ; :: thesis: |.(y - x).| < r
then ex p being Point of (TOP-REAL n) st
( y = p & |.(p - x).| < r ) ;
hence |.(y - x).| < r ; :: thesis: verum

end;

thus ( |.(y - x).| < r implies y in Ball x,r ) ; :: thesis: verum