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