for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||