for X being ComplexUnitarySpace
for x, y, u, v being Point of X holds dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v))