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

proof

assume w in Sphere (x,r) ; :: thesis: dist (x,w) = r
then ||.(x - w).|| = r by Th51;
hence dist (x,w) = r by CSSPACE:def 16; :: thesis: verum

end;

assume dist (x,w) = r ; :: thesis: w in Sphere (x,r)
then ||.(x - w).|| = r by CSSPACE:def 16;
hence w in Sphere (x,r) ; :: thesis: verum