for x, y being R_eal holds |.(x - y).| = |.(y - x).|