let x, y be R_eal; :: thesis: y - x <= |.(x - y).|
( x - y <= |.(x - y).| & - |.(x - y).| <= x - y ) by EXTREAL2:57;
then ( x - y <= |.(x - y).| & - (x - y) <= |.(x - y).| ) by XXREAL_3:71;
hence y - x <= |.(x - y).| by XXREAL_3:27; :: thesis: verum