theorem :: XXREAL_2:12

for x, y being ExtReal holds max (x,y) = max {x,y}