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;

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 )
;

end;

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;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

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;r1 - r2 <= s2 - s1 by A2, XREAL_1:13;

hence |.(r1 - r2).| <= s2 - s1 by A6, ABSVALUE:def 1; :: thesis: verum