let a, c, b be real number ; :: thesis: ( a > 0 & a <= 1 & c >= b implies a #R c <= a #R b )
assume A1: ( a > 0 & a <= 1 & c >= b ) ; :: thesis: a #R c <= a #R b
then A2: 1 / a >= 1 by Lm4, XREAL_1:87;
a #R b > 0 by A1, Th95;
then (a #R b) " > 0 ;
then A3: 1 / (a #R b) > 0 ;
(1 / a) #R c >= (1 / a) #R b by A1, A2, Th96;
then 1 / (a #R c) >= (1 / a) #R b by A1, Th93;
then 1 / (a #R c) >= 1 / (a #R b) by A1, Th93;
hence a #R c <= a #R b by A3, XREAL_1:91; :: thesis: verum