let X be RealUnitarySpace; :: thesis: for z, x being Point of X
for r being Real holds
( z in Ball x,r iff ||.(x - z).|| < r )
let z, x be Point of X; :: thesis: for r being Real holds
( z in Ball x,r iff ||.(x - z).|| < r )
let r be Real; :: thesis: ( z in Ball x,r iff ||.(x - z).|| < r )
thus ( z in Ball x,r implies ||.(x - z).|| < r ) :: thesis: ( ||.(x - z).|| < r implies z in Ball x,r )

proof

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

end;

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