theorem :: CLVECT_2:42

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