theorem :: XXREAL_0:16

for a, b being ExtReal holds
( max (a,b) = a or max (a,b) = b ) by Def9;