let a, b, c be ExtReal; :: 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