let a, b be real number ; :: thesis: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 implies a * b <= 1 )
assume A1: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 ) ; :: thesis: a * b <= 1
then a * b <= 1 * a by Lm12;
hence a * b <= 1 by A1, XXREAL_0:2; :: thesis: verum