let n be Nat; :: thesis: for r being Real
for x, y being Point of (TOP-REAL n) holds
( y in cl_Ball (x,r) iff |.(y - x).| <= r )
let r be Real; :: thesis: for x, y being Point of (TOP-REAL n) holds
( y in cl_Ball (x,r) iff |.(y - x).| <= r )
let x, y be Point of (TOP-REAL n); :: thesis: ( y in cl_Ball (x,r) iff |.(y - x).| <= r )

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

assume y in cl_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 cl_Ball (x,r) ) ; :: thesis: verum