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