let a, b be real number ; :: thesis: ( a > 1 & b < 0 implies a #R b < 1 )
assume A1: ( a > 1 & b < 0 ) ; :: thesis: a #R b < 1
then - b > 0 by XREAL_1:60;
then a #R (- b) > 1 by A1, Th100;
then 1 / (a #R b) > 1 by A1, Th90;
then 1 / (1 / (a #R b)) < 1 by XREAL_1:214;
hence a #R b < 1 ; :: thesis: verum