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