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