theorem Th3: :: NORMSP_1:3

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