let b, c, a be ext-real number ; :: 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