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