let a, c, b be real number ; :: thesis: ( a > 1 & c > b implies a #R c > a #R b )
assume A1: ( a > 1 & c > b ) ; :: thesis: a #R c > a #R b
then consider p being Rational such that
A2: ( b < p & p < c ) by RAT_1:22;
consider q being Rational such that
A3: ( b < q & q < p ) by A2, RAT_1:22;
A4: a #Q q < a #Q p by A1, A3, Th75;
consider s1 being Rational_Sequence such that
A5: ( s1 is convergent & c = lim s1 & ( for n being Element of NAT holds s1 . n >= c ) ) by Th80;
consider s2 being Rational_Sequence such that
A6: ( s2 is convergent & b = lim s2 & ( for n being Element of NAT holds s2 . n <= b ) ) by Th79;
A7: a #Q s1 is convergent by A1, A5, Th82;
A8: a #Q s2 is convergent by A1, A6, Th82;

now

let n be Element of NAT ; :: thesis: (a #Q s1) . n >= a #Q p
s1 . n >= c by A5;
then s1 . n >= p by A2, XXREAL_0:2;
then a #Q (s1 . n) >= a #Q p by A1, Th74;
hence (a #Q s1) . n >= a #Q p by Def7; :: thesis: verum

end;

then lim (a #Q s1) >= a #Q p by A7, Th2;
then A9: a #R c >= a #Q p by A1, A5, A7, Def8;

now

let n be Element of NAT ; :: thesis: (a #Q s2) . n <= a #Q q
s2 . n <= b by A6;
then s2 . n <= q by A3, XXREAL_0:2;
then a #Q (s2 . n) <= a #Q q by A1, Th74;
hence (a #Q s2) . n <= a #Q q by Def7; :: thesis: verum

end;

then lim (a #Q s2) <= a #Q q by A8, Th3;
then a #R b <= a #Q q by A1, A6, A8, Def8;
then a #R b < a #Q p by A4, XXREAL_0:2;
hence a #R c > a #R b by A9, XXREAL_0:2; :: thesis: verum