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