theorem :: CLVECT_2:46

for X being ComplexUnitarySpace
for x, y being Point of X
for q, r being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)