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