let a, b, c, d, e be Real; :: thesis: ( a <= b & b <= c & |.(a - d).| <= e & |.(c - d).| <= e implies |.(b - d).| <= e )
assume that
A1: ( a <= b & b <= c ) and
A2: |.(a - d).| <= e and
A3: |.(c - d).| <= e ; :: thesis: |.(b - d).| <= e
( b in [.a,c.] & a <= c ) by A1, XXREAL_1:1, XXREAL_0:2;
then consider r being Real such that
A4: ( 0 <= r & r <= 1 ) and
A5: b = (r * a) + ((1 - r) * c) by SPRECT_1:51;
A6: |.((r * (a - d)) + ((1 - r) * (c - d))).| <= |.(r * (a - d)).| + |.((1 - r) * (c - d)).| by COMPLEX1:56;
|.(r * (a - d)).| = |.r.| * |.(a - d).| by COMPLEX1:65
.= r * |.(a - d).| by A4, ABSVALUE:def 1 ;
then A7: |.(r * (a - d)).| <= r * e by A4, A2, XREAL_1:64;
A8: r - r <= 1 - r by A4, XREAL_1:9;
|.((1 - r) * (c - d)).| = |.(1 - r).| * |.(c - d).| by COMPLEX1:65
.= (1 - r) * |.(c - d).| by A8, ABSVALUE:def 1 ;
then A9: |.((1 - r) * (c - d)).| <= (1 - r) * e by A8, A3, XREAL_1:64;
|.(b - d).| <= (r * e) + |.((1 - r) * (c - d)).| by A5, A6, A7, Lm01;
then |.(b - d).| <= (r * e) + ((1 - r) * e) by A9, Lm01;
hence |.(b - d).| <= e ; :: thesis: verum