theorem MinMax: :: NEWTON03:41

for a, b being Real holds a + b = (min (a,b)) + (max (a,b))