theorem :: XXREAL_0:31

for a, b, c being ExtReal st max (b,c) < a holds
b < a