theorem Th16: :: EUCLID:19

for n being Nat
for x, x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|