let a, b, c be ExtReal; :: thesis: ( max (b,c) < a implies b < a )
b <= max (b,c) by Th25;
hence ( max (b,c) < a implies b < a ) by Th2; :: thesis: verum