theorem Th9: :: NORMSP_1:9

for RNS being RealNormSpace
for x, y being Point of RNS holds |.(||.x.|| - ||.y.||).| <= ||.(x - y).||