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