let a, b be Real; :: thesis: ( 0 < a & b < 1 implies a * b < a )
assume that
A1: a > 0 and
A2: b < 1 ; :: thesis: a * b < a
a * b < a * 1 by A1, A2, Lm13;
hence a * b < a ; :: thesis: verum