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

proof

assume w in Sphere 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 Sphere x,r
hence w in Sphere x,r ; :: thesis: verum