theorem Th109: :: CLVECT_1:109

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