let a, b, c, d be Real; :: thesis: |.((min (c,(max (d,a)))) - (min (c,(max (d,b))))).| <= |.(a - b).|
A1: |.((min (c,(max (d,a)))) - (min (c,(max (d,b))))).| <= |.((max (d,a)) - (max (d,b))).| by F51min;
|.((max (d,a)) - (max (d,b))).| <= |.(a - b).| by F51max;
hence |.((min (c,(max (d,a)))) - (min (c,(max (d,b))))).| <= |.(a - b).| by A1, XXREAL_0:2; :: thesis: verum