let a, b be Real; :: thesis: ( a > 1 & b < 0 implies a #R b < 1 )
assume that
A1: a > 1 and
A2: b < 0 ; :: thesis: a #R b < 1
- b > 0 by A2;
then a #R (- b) > 1 by A1, Th86;
then 1 / (a #R b) > 1 by A1, Th76;
then 1 / (1 / (a #R b)) < 1 by XREAL_1:212;
hence a #R b < 1 ; :: thesis: verum