let a, b, c, d be Real; :: thesis: ( a < c & c < b & a < d & d < b implies |.(d - c).| < b - a )
assume that
A1: a < c and
A2: ( c < b & a < d ) and
A3: d < b ; :: thesis: |.(d - c).| < b - a
A4: c + a < b + d by A2, XREAL_1:8;
then c - d <= b - a by XREAL_1:21;
then A5: - (b - a) <= - (c - d) by XREAL_1:24;
A6: a + d < c + b by A1, A3, XREAL_1:8;
A7: |.(d - c).| <> b - a

proof

assume A8: |.(d - c).| = b - a ; :: thesis: contradiction
A9: ( d - c = b - a or d - c = - (b - a) )

proof

per cases ( 0 <= d - c or not 0 <= d - c ) ;

suppose 0 <= d - c ; :: thesis: ( d - c = b - a or d - c = - (b - a) )

hence ( d - c = b - a or d - c = - (b - a) ) by A8, ABSVALUE:def 1; :: thesis: verum

end;

suppose not 0 <= d - c ; :: thesis: ( d - c = b - a or d - c = - (b - a) )

then b - a = - (d - c) by A8, ABSVALUE:def 1;
hence ( d - c = b - a or d - c = - (b - a) ) ; :: thesis: verum

end;

end;

end;

now :: thesis: ( ( d - c = b - a & contradiction ) or ( d - c = - (b - a) & contradiction ) )

per cases ( d - c = b - a or d - c = - (b - a) ) by A9;

case d - c = b - a ; :: thesis: contradiction

hence contradiction by A6; :: thesis: verum

end;

case d - c = - (b - a) ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

d - c < b - a by A6, XREAL_1:21;
then |.(d - c).| <= b - a by A5, ABSVALUE:5;
hence |.(d - c).| < b - a by A7, XXREAL_0:1; :: thesis: verum