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 ( a <= b & c <= d ) ; :: thesis: (abs (b - a)) + (abs (d - c)) = (b - a) + (d - c)
then ( a - a <= b - a & c - c <= d - c ) by XREAL_1:15;
then ( abs (b - a) = b - a & abs (d - c) = d - c ) by ABSVALUE:def 1;
hence (abs (b - a)) + (abs (d - c)) = (b - a) + (d - c) ; :: thesis: verum