for X being ComplexUnitarySpace
for x, y, w being Point of X
for r being Real st y in Ball (x,r) & w in Ball (x,r) holds
dist (y,w) < 2 * r