for X being ComplexUnitarySpace
for x, y being Point of X
for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)