let a, b, c be Real; ( a - b <= c & b <= a implies |.(b - a).| <= c )
assume that
A1:
a - b <= c
and
A2:
b <= a
; |.(b - a).| <= c
b - b <= a - b
by A2, XREAL_1:9;
then A3:
0 <= c
by A1;
(- 1) * c <= (- 1) * (a - b)
by A1, XREAL_1:65;
then A5:
- c <= b - a
;
b - a <= a - a
by A2, XREAL_1:9;
hence
|.(b - a).| <= c
by ABSVALUE:5, A5, A3; verum