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