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