let a, b, c be ext-real number ; :: thesis: ( a <= min b,c implies a <= b )
min b,c <= b by Th17;
hence ( a <= min b,c implies a <= b ) by Th2; :: thesis: verum