let a, b, c be Real; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

per cases ( ( a >= b & b >= c ) or ( a >= c & c >= b ) or ( b >= c & c >= a ) or ( b >= a & a >= c ) or ( c >= a & a >= b ) or ( c >= b & b >= a ) ) ;

suppose A1: ( a >= b & b >= c ) ; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

then |.((max (c,a)) - (max (c,b))).| = |.(a - (max (c,b))).| by XXREAL_0:def 10, XXREAL_0:2;
hence |.((max (c,a)) - (max (c,b))).| <= |.(a - b).| by XXREAL_0:def 10, A1; :: thesis: verum

end;

suppose A2: ( a >= c & c >= b ) ; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

then a >= b by XXREAL_0:2;
then a - b >= b - b by XREAL_1:13;
then A24: |.(a - b).| = a - b by ABSVALUE:def 1;
A21: a - c >= c - c by A2, XREAL_1:13;
|.((max (c,a)) - (max (c,b))).| = |.(a - (max (c,b))).| by XXREAL_0:def 10, A2
.= |.(a - c).| by XXREAL_0:def 10, A2
.= a - c by ABSVALUE:def 1, A21 ;
hence |.((max (c,a)) - (max (c,b))).| <= |.(a - b).| by A24, A2, XREAL_1:13; :: thesis: verum

end;

suppose A3: ( b >= c & c >= a ) ; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

then b >= a by XXREAL_0:2;
then AA: b - a >= a - a by XREAL_1:13;
A32: |.(a - b).| = |.(b - a).| by COMPLEX1:60
.= b - a by ABSVALUE:def 1, AA ;
A33: b - c >= c - c by A3, XREAL_1:13;
|.((max (c,a)) - (max (c,b))).| = |.(c - (max (c,b))).| by XXREAL_0:def 10, A3
.= |.(c - b).| by XXREAL_0:def 10, A3
.= |.(b - c).| by COMPLEX1:60
.= b - c by ABSVALUE:def 1, A33 ;
hence |.((max (c,a)) - (max (c,b))).| <= |.(a - b).| by A32, A3, XREAL_1:13; :: thesis: verum

end;

suppose A4: ( b >= a & a >= c ) ; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

then |.((max (c,a)) - (max (c,b))).| = |.((max (c,a)) - b).| by XXREAL_0:def 10, XXREAL_0:2
.= |.(a - b).| by XXREAL_0:def 10, A4 ;
hence |.((max (c,a)) - (max (c,b))).| <= |.(a - b).| ; :: thesis: verum

end;

suppose A5: ( c >= a & a >= b ) ; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

then |.((max (c,a)) - (max (c,b))).| = |.((max (c,a)) - c).| by XXREAL_0:def 10, XXREAL_0:2
.= |.(c - c).| by XXREAL_0:def 10, A5
.= 0 by COMPLEX1:44 ;
hence |.((max (c,a)) - (max (c,b))).| <= |.(a - b).| by COMPLEX1:46; :: thesis: verum

end;

suppose A6: ( c >= b & b >= a ) ; :: thesis: |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

then |.((max (c,a)) - (max (c,b))).| = |.(c - (max (c,b))).| by XXREAL_0:def 10, XXREAL_0:2
.= |.(c - c).| by XXREAL_0:def 10, A6
.= 0 by COMPLEX1:44 ;
hence |.((max (c,a)) - (max (c,b))).| <= |.(a - b).| by COMPLEX1:46; :: thesis: verum

end;

end;