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