let a, b be Real; :: thesis: ( a < 0 & b < 1 implies a < a * b )
assume that
A1: a < 0 and
A2: b < 1 ; :: thesis: a < a * b
a * b > a * 1 by A1, A2, Lm24;
hence a < a * b ; :: thesis: verum