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 Lm13;
hence a * b > 1 by A1, XXREAL_0:2; :: thesis: verum