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