let a, b be real number ; :: thesis: ( 0 <= a & 1 <= b implies a <= a * b )
assume ( a >= 0 & b >= 1 ) ; :: thesis: a <= a * b
then a * b >= a * 1 by Lm12;
hence a * b >= a ; :: thesis: verum