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