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