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