let a, b, c be Real; :: thesis: |.((min (c,a)) - (min (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: |.((min (c,a)) - (min (c,b))).| <= |.(a - b).|

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

end;

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

then a <= b by XXREAL_0:2;
then A22: a - a <= b - a by XREAL_1:13;
A24: |.(a - b).| = |.(b - a).| by COMPLEX1:60
.= b - a by ABSVALUE:def 1, A22 ;
A21: a - a <= c - a by A2, XREAL_1:13;
|.((min (c,a)) - (min (c,b))).| = |.(a - (min (c,b))).| by XXREAL_0:def 9, A2
.= |.(a - c).| by XXREAL_0:def 9, A2
.= |.(c - a).| by COMPLEX1:60
.= c - a by ABSVALUE:def 1, A21 ;
hence |.((min (c,a)) - (min (c,b))).| <= |.(a - b).| by A24, A2, XREAL_1:13; :: thesis: verum

end;

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

then b <= a by XXREAL_0:2;
then b - b <= a - b by XREAL_1:13;
then A32: |.(a - b).| = a - b by ABSVALUE:def 1;
A33: b - b <= c - b by A3, XREAL_1:13;
|.((min (c,a)) - (min (c,b))).| = |.(c - (min (c,b))).| by XXREAL_0:def 9, A3
.= |.(c - b).| by XXREAL_0:def 9, A3
.= c - b by ABSVALUE:def 1, A33 ;
hence |.((min (c,a)) - (min (c,b))).| <= |.(a - b).| by A32, A3, XREAL_1:13; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

end;