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