theorem Th3: :: SPPOL_1:3

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