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