let a, b, c, d be Real; :: thesis: |.((max (c,(min (d,a)))) - (max (c,(min (d,b))))).| <= |.(a - b).|
A1: |.((max (c,(min (d,a)))) - (max (c,(min (d,b))))).| = |.((((c + (min (d,a))) + |.(c - (min (d,a))).|) / 2) - (max (c,(min (d,b))))).| by COMPLEX1:74
.= |.((((c + (min (d,a))) + |.(c - (min (d,a))).|) / 2) - (((c + (min (d,b))) + |.(c - (min (d,b))).|) / 2)).| by COMPLEX1:74
.= |.(((((min (d,a)) - (min (d,b))) + |.(c - (min (d,a))).|) - |.(c - (min (d,b))).|) / 2).|
.= |.(((((((d + a) - |.(d - a).|) / 2) - (min (d,b))) + |.(c - (min (d,a))).|) - |.(c - (min (d,b))).|) / 2).| by COMPLEX1:73
.= |.(((((((d + a) - |.(d - a).|) / 2) - (((d + b) - |.(d - b).|) / 2)) + |.(c - (min (d,a))).|) - |.(c - (min (d,b))).|) / 2).| by COMPLEX1:73
.= |.((((((a - b) - |.(d - a).|) + |.(d - b).|) / 2) + |.(c - (min (d,a))).|) - |.(c - (min (d,b))).|).| / |.2.| by COMPLEX1:67
.= |.(((((a - b) - |.(d - a).|) + |.(d - b).|) / 2) + (|.(c - (min (d,a))).| - |.(c - (min (d,b))).|)).| / 2 by COMPLEX1:43 ;
A2a: |.(((((a - b) - |.(d - a).|) + |.(d - b).|) / 2) + (|.(c - (min (d,a))).| - |.(c - (min (d,b))).|)).| / 2 <= (|.((((a - b) - |.(d - a).|) + |.(d - b).|) / 2).| + |.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).|) / 2 by XREAL_1:72, COMPLEX1:56;
A4: |.((((a - b) - |.(d - a).|) + |.(d - b).|) / 2).| = |.((a - b) - (|.(d - a).| - |.(d - b).|)).| / |.2.| by COMPLEX1:67
.= |.((a - b) - (|.(d - a).| - |.(d - b).|)).| / 2 by COMPLEX1:43 ;
A3: |.((a - b) - (|.(d - a).| - |.(d - b).|)).| <= |.(a - b).| + |.(|.(d - a).| - |.(d - b).|).| by COMPLEX1:57;
|.(|.(d - a).| - |.(d - b).|).| <= |.((d - a) - (d - b)).| by COMPLEX1:64;
then |.(|.(d - a).| - |.(d - b).|).| <= |.(b - a).| ;
then |.(|.(d - a).| - |.(d - b).|).| <= |.(a - b).| by COMPLEX1:60;
then |.(a - b).| + |.(|.(d - a).| - |.(d - b).|).| <= |.(a - b).| + |.(a - b).| by XREAL_1:6;
then |.((a - b) - (|.(d - a).| - |.(d - b).|)).| <= |.(a - b).| + |.(a - b).| by XXREAL_0:2, A3;
then |.((((a - b) - |.(d - a).|) + |.(d - b).|) / 2).| <= (|.(a - b).| + |.(a - b).|) / 2 by A4, XREAL_1:72;
then A5: |.((((a - b) - |.(d - a).|) + |.(d - b).|) / 2).| / 2 <= |.(a - b).| / 2 by XREAL_1:72;
|.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).| <= |.((c - (min (d,a))) - (c - (min (d,b)))).| by COMPLEX1:64;
then |.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).| <= |.((min (d,b)) - (min (d,a))).| ;
then A6a: |.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).| <= |.((min (d,a)) - (min (d,b))).| by COMPLEX1:60;
|.((min (d,a)) - (min (d,b))).| / 2 = |.((((d + a) - |.(d - a).|) / 2) - (min (d,b))).| / 2 by COMPLEX1:73
.= |.((((d + a) - |.(d - a).|) / 2) - (((d + b) - |.(d - b).|) / 2)).| / 2 by COMPLEX1:73
.= |.((((d + a) - |.(d - a).|) - ((d + b) - |.(d - b).|)) / 2).| / 2
.= (|.(((a - |.(d - a).|) - b) + |.(d - b).|).| / |.2.|) / 2 by COMPLEX1:67
.= (|.(((a - |.(d - a).|) - b) + |.(d - b).|).| / 2) / 2 by COMPLEX1:43
.= |.((a - b) - (|.(d - a).| - |.(d - b).|)).| / 4 ;
then A8: |.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).| / 2 <= |.((a - b) - (|.(d - a).| - |.(d - b).|)).| / 4 by A6a, XREAL_1:72;
A7: |.((a - b) - (|.(d - a).| - |.(d - b).|)).| <= |.(a - b).| + |.(|.(d - a).| - |.(d - b).|).| by COMPLEX1:57;
|.(|.(d - a).| - |.(d - b).|).| <= |.((d - a) - (d - b)).| by COMPLEX1:64;
then |.(|.(d - a).| - |.(d - b).|).| <= |.(b - a).| ;
then |.(|.(d - a).| - |.(d - b).|).| <= |.(a - b).| by COMPLEX1:60;
then |.(a - b).| + |.(|.(d - a).| - |.(d - b).|).| <= |.(a - b).| + |.(a - b).| by XREAL_1:6;
then |.((a - b) - (|.(d - a).| - |.(d - b).|)).| <= |.(a - b).| + |.(a - b).| by XXREAL_0:2, A7;
then |.((a - b) - (|.(d - a).| - |.(d - b).|)).| / 4 <= (|.(a - b).| + |.(a - b).|) / 4 by XREAL_1:72;
then |.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).| / 2 <= (|.(a - b).| + |.(a - b).|) / 4 by A8, XXREAL_0:2;
then (|.((((a - b) - |.(d - a).|) + |.(d - b).|) / 2).| / 2) + (|.(|.(c - (min (d,a))).| - |.(c - (min (d,b))).|).| / 2) <= (|.(a - b).| / 2) + ((|.(a - b).| + |.(a - b).|) / 4) by XREAL_1:7, A5;
hence |.((max (c,(min (d,a)))) - (max (c,(min (d,b))))).| <= |.(a - b).| by A2a, A1, XXREAL_0:2; :: thesis: verum