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