for n being Nat
for x, y being Element of REAL n holds abs (x - y) = abs (y - x)