theorem :: XXREAL_0:28

for a, b, c being ExtReal st b <= a & c <= a holds
max (b,c) <= a by Def9;