let a, b, r1, r2 be Real; :: thesis: ( a <= r1 & r1 <= b & a <= r2 & r2 <= b implies |.(r1 - r2).| <= b - a )
assume that
A1: a <= r1 and
A2: ( r1 <= b & a <= r2 ) and
A3: r2 <= b ; :: thesis: |.(r1 - r2).| <= b - a

per cases ( r1 - r2 >= 0 or r1 - r2 < 0 ) ;

suppose A4: r1 - r2 >= 0 ; :: thesis: |.(r1 - r2).| <= b - a

A5: ( r1 - r2 <= b - r2 & b - r2 <= b - a ) by A2, XREAL_1:9, XREAL_1:10;
|.(r1 - r2).| = r1 - r2 by A4, ABSVALUE:def 1;
hence |.(r1 - r2).| <= b - a by A5, XXREAL_0:2; :: thesis: verum

end;

suppose r1 - r2 < 0 ; :: thesis: |.(r1 - r2).| <= b - a

then A6: |.(r1 - r2).| = - (r1 - r2) by ABSVALUE:def 1
.= r2 - r1 ;
( r2 - r1 <= b - r1 & b - r1 <= b - a ) by A1, A3, XREAL_1:9, XREAL_1:10;
hence |.(r1 - r2).| <= b - a by A6, XXREAL_0:2; :: thesis: verum

end;

end;