theorem Th10: :: NORMSP_1:10

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