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