for X being ComplexUnitarySpace
for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball (x,r)