theorem SAD: :: COMPLEX3:38
for a, b, c, d being positive Real st a + b = c + d holds
(max (a,b)) - (max (c,d)) = (min (c,d)) - (min (a,b))