theorem Th8: :: NORMSP_1:8

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