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