theorem :: NEWTON04:17

for x, y being Real holds (max (x,y)) - (min (x,y)) = |.(x - y).|