let X be ComplexUnitarySpace; :: thesis: for w, x being Point of X
for r being Real holds
( w in Sphere x,r iff dist x,w = r )
let w, x 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