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