let a, b, c be real number ; :: thesis: ( |.(a - b).| <= c implies ( b - c <= a & a <= b + c ) )
assume A1: |.(a - b).| <= c ; :: thesis: ( b - c <= a & a <= b + c )
A2: |.(a - b).| >= 0 by COMPLEX1:132;
then A3: ( b <= b + c & b >= b - c ) by A1, XREAL_1:33, XREAL_1:45;

per cases ( a - b >= 0 or a - b < 0 ) ;

suppose A4: a - b >= 0 ; :: thesis: ( b - c <= a & a <= b + c )

then A5: |.(a - b).| = a - b by ABSVALUE:def 1;
a >= 0 + b by A4, XREAL_1:21;
hence ( b - c <= a & a <= b + c ) by A1, A3, A5, XREAL_1:22, XXREAL_0:2; :: thesis: verum

end;

suppose a - b < 0 ; :: thesis: ( b - c <= a & a <= b + c )

then A6: |.(a - b).| = - (a - b) by ABSVALUE:def 1
.= b - a ;
then 0 + a <= b by A2, XREAL_1:21;
hence ( b - c <= a & a <= b + c ) by A1, A3, A6, XREAL_1:14, XXREAL_0:2; :: thesis: verum

end;

end;