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