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