let a, b be Real; :: thesis: ( 0 <= a & a < 1 & b <= 1 implies a * b < 1 )
assume that
A1: 0 <= a and
A2: a < 1 and
A3: b <= 1 ; :: thesis: a * b < 1
a * b <= 1 * a by A1, A3, Lm12;
hence a * b < 1 by A2, XXREAL_0:2; :: thesis: verum