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