let a, b, c, d be Real; :: thesis: ( a < c & c < b & a < d & d < b implies abs (d - c) < b - a )
assume A1: ( a < c & c < b & a < d & d < b ) ; :: thesis: abs (d - c) < b - a
then A2: a + d < c + b by XREAL_1:10;
then A3: d - c < b - a by XREAL_1:23;
A4: c + a < b + d by A1, XREAL_1:10;
then ( c - d <> b - a & c - d <= b - a ) by XREAL_1:23;
then - (b - a) <= - (c - d) by XREAL_1:26;
then A5: abs (d - c) <= b - a by A3, ABSVALUE:12;
abs (d - c) <> b - a

proof

assume A6: abs (d - c) = b - a ; :: thesis: contradiction
A7: ( 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 A6, 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 A6, ABSVALUE:def 1;
hence ( d - c = b - a or d - c = - (b - a) ) ; :: thesis: verum

end;

end;

end;

now

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

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

hence contradiction by A2; :: thesis: verum

end;

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

hence contradiction by A4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence abs (d - c) < b - a by A5, XXREAL_0:1; :: thesis: verum