let X be RealUnitarySpace; for x, z being Point of X
for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )
let x, z be Point of X; for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )
let r be Real; ( z in cl_Ball (x,r) iff dist (x,z) <= r )
thus
( z in cl_Ball (x,r) implies dist (x,z) <= r )
( dist (x,z) <= r implies z in cl_Ball (x,r) )
assume
dist (x,z) <= r
; z in cl_Ball (x,r)
then
||.(x - z).|| <= r
by BHSP_1:def 5;
hence
z in cl_Ball (x,r)
; verum