let a, b, c be Real; ( a > 0 & a <= 1 & c >= b implies a #R c <= a #R b )
assume that
A1:
a > 0
and
A2:
a <= 1
and
A3:
c >= b
; a #R c <= a #R b
1 / a >= 1
by A1, A2, Lm4, XREAL_1:85;
then
(1 / a) #R c >= (1 / a) #R b
by A3, Th82;
then
1 / (a #R c) >= (1 / a) #R b
by A1, Th79;
then A4:
1 / (a #R c) >= 1 / (a #R b)
by A1, Th79;
a #R b > 0
by A1, Th81;
hence
a #R c <= a #R b
by A4, XREAL_1:89; verum