theorem Th110: :: CLVECT_1:110

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