let X be RealUnitarySpace; :: thesis: for z, x being Point of X
for r being Real holds
( z in cl_Ball x,r iff dist x,z <= r )
let z, x be Point of X; :: thesis: for r being Real holds
( z in cl_Ball x,r iff dist x,z <= r )
let r be Real; :: thesis: ( z in cl_Ball x,r iff dist x,z <= r )
thus ( z in cl_Ball x,r implies dist x,z <= r ) :: thesis: ( dist x,z <= r implies z in cl_Ball x,r )

proof

assume z in cl_Ball x,r ; :: thesis: dist x,z <= r
then ||.(x - z).|| <= r by Th47;
hence dist x,z <= r by BHSP_1:def 5; :: thesis: verum

end;

assume dist x,z <= r ; :: thesis: z in cl_Ball x,r
then ||.(x - z).|| <= r by BHSP_1:def 5;
hence z in cl_Ball x,r ; :: thesis: verum