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