let a, b be real number ; :: thesis: ( a < 0 & b < 1 implies a < a * b )
assume ( a < 0 & b < 1 ) ; :: thesis: a < a * b
then a * b > a * 1 by Lm25;
hence a < a * b ; :: thesis: verum