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