let r1, r2, s1, s2 be Real; :: thesis: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] implies abs (r1 - r2) <= s2 - s1 )
assume A1: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] ) ; :: thesis: abs (r1 - r2) <= s2 - s1
then A2: ( r1 <= s2 & s1 <= r2 ) by Lm6;
A3: ( s1 <= r1 & r2 <= s2 ) by A1, Lm6;

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

suppose A4: r1 <= r2 ; :: thesis: abs (r1 - r2) <= s2 - s1

A5: r2 - r1 <= s2 - s1 by A3, XREAL_1:15;
r2 - r1 >= 0 by A4, XREAL_1:50;
then abs (r2 - r1) <= s2 - s1 by A5, ABSVALUE:def 1;
hence abs (r1 - r2) <= s2 - s1 by Th13; :: thesis: verum

end;

suppose r1 > r2 ; :: thesis: abs (r1 - r2) <= s2 - s1

then A6: r1 - r2 >= 0 by XREAL_1:50;
r1 - r2 <= s2 - s1 by A2, XREAL_1:15;
hence abs (r1 - r2) <= s2 - s1 by A6, ABSVALUE:def 1; :: thesis: verum

end;

end;