theorem :: EXTREAL1:39

for x, y being ExtReal holds (min (x,y)) + (max (x,y)) = x + y