let a, b be real number ; :: thesis: ( a >= 1 & b <= 0 implies a #R b <= 1 )
assume that
A1: a >= 1 and
A2: b <= 0 ; :: thesis: a #R b <= 1
a #R (- b) >= 1 by A1, A2, Th99;
then 1 / (a #R b) >= 1 by A1, Th90;
then 1 / (1 / (a #R b)) <= 1 by XREAL_1:213;
hence a #R b <= 1 ; :: thesis: verum