for X being ComplexUnitarySpace
for x, w being Point of X
for r being Real holds
( w in Sphere (x,r) iff dist (x,w) = r )