theorem Th104: :: CLVECT_1:104

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