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 EXTREAL2:47;
hence y - x <= |.(x - y).| by EXTREAL2:15; :: thesis: verum