theorem :: EXTREAL1:37

for x, y being ExtReal st x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds
min (x,y) = ((x + y) - |.(x - y).|) / 2