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