theorem :: CSSPACE:49

for X being ComplexUnitarySpace
for x, y being Point of X holds |.(||.x.|| - ||.y.||).| <= ||.(x - y).||