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