let r1, r2, s1, s2 be Real; :: thesis: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] implies |.(r1 - r2).| <= s2 - s1 )
assume A1: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] ) ; :: thesis: |.(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: |.(r1 - r2).| <= s2 - s1

A5: r2 - r1 <= s2 - s1 by A3, XREAL_1:13;
r2 - r1 >= 0 by A4, XREAL_1:48;
then |.(r2 - r1).| <= s2 - s1 by A5, ABSVALUE:def 1;
hence |.(r1 - r2).| <= s2 - s1 by Th11; :: thesis: verum

end;

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

then A6: r1 - r2 >= 0 by XREAL_1:48;
r1 - r2 <= s2 - s1 by A2, XREAL_1:13;
hence |.(r1 - r2).| <= s2 - s1 by A6, ABSVALUE:def 1; :: thesis: verum

end;

end;