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