theorem :: TOPREAL6:14

for a, b, c, d being Real st a <= b & c <= d holds
|.(b - a).| + |.(d - c).| = (b - a) + (d - c)