let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies |.(b - a).| + |.(d - c).| = (b - a) + (d - c) )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: |.(b - a).| + |.(d - c).| = (b - a) + (d - c)
a - a <= b - a by A1, XREAL_1:13;
then A3: |.(b - a).| = b - a by ABSVALUE:def 1;
c - c <= d - c by A2, XREAL_1:13;
hence |.(b - a).| + |.(d - c).| = (b - a) + (d - c) by A3, ABSVALUE:def 1; :: thesis: verum