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