let a, b, r1, r2 be Real; :: thesis: ( a <= r1 & r1 <= b & a <= r2 & r2 <= b implies abs (r1 - r2) <= b - a )
assume A1: ( a <= r1 & r1 <= b & a <= r2 & r2 <= b ) ; :: thesis: abs (r1 - r2) <= b - a

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

suppose r1 - r2 >= 0 ; :: thesis: abs (r1 - r2) <= b - a

then A2: abs (r1 - r2) = r1 - r2 by ABSVALUE:def 1;
A3: r1 - r2 <= b - r2 by A1, XREAL_1:11;
b - r2 <= b - a by A1, XREAL_1:12;
hence abs (r1 - r2) <= b - a by A2, A3, XXREAL_0:2; :: thesis: verum

end;

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

then A4: abs (r1 - r2) = - (r1 - r2) by ABSVALUE:def 1
.= r2 - r1 ;
A5: r2 - r1 <= b - r1 by A1, XREAL_1:11;
b - r1 <= b - a by A1, XREAL_1:12;
hence abs (r1 - r2) <= b - a by A4, A5, XXREAL_0:2; :: thesis: verum

end;

end;