let x, y be R_eal; :: thesis: y - x <= |.(x - y).|
- |.(x - y).| <= x - y by EXTREAL1:20;
then - (x - y) <= |.(x - y).| by XXREAL_3:60;
hence y - x <= |.(x - y).| by XXREAL_3:26; :: thesis: verum