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