let a, b, c be Real; :: 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:46;
then A3: b <= b + c by A1, XREAL_1:31;
A4: b >= b - c by A1, A2, XREAL_1:43;
per cases ( a - b >= 0 or a - b < 0 ) ;
suppose a - b >= 0 ; :: thesis: ( b - c <= a & a <= b + c )
then ( |.(a - b).| = a - b & a >= 0 + b ) by ABSVALUE:def 1, XREAL_1:19;
hence ( b - c <= a & a <= b + c ) by A1, A4, XREAL_1:20, XXREAL_0:2; :: thesis: verum
end;
suppose a - b < 0 ; :: thesis: ( b - c <= a & a <= b + c )
then A5: |.(a - b).| = - (a - b) by ABSVALUE:def 1
.= b - a ;
then 0 + a <= b by A2, XREAL_1:19;
hence ( b - c <= a & a <= b + c ) by A1, A3, A5, XREAL_1:12, XXREAL_0:2; :: thesis: verum
end;
end;