theorem :: CLVECT_2:44
for X being ComplexUnitarySpace
for x, y, w being Point of X
for r being Real st y in Ball (x,r) holds
y - w in Ball ((x - w),r)