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, Lm28;
hence a * b <= a ; :: thesis: verum