let a, b, c be Real; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

assume that

A1: a > 0 and

A2: a <= 1 and

A3: c >= b ; :: thesis: 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; :: thesis: verum