let X be ComplexUnitarySpace; :: thesis: for x, w being Point of X
for r being Real holds
( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
let x, w be Point of X; :: thesis: for r being Real holds
( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
let r be Real; :: thesis: ( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
thus ( w in cl_Ball (x,r) implies ||.(x - w).|| <= r ) :: thesis: ( ||.(x - w).|| <= r implies w in cl_Ball (x,r) )

proof

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

end;

assume ||.(x - w).|| <= r ; :: thesis: w in cl_Ball (x,r)
hence w in cl_Ball (x,r) ; :: thesis: verum