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
consider s1 being Rational_Sequence such that
A2: ( 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
A3: ( s2 is convergent & b = lim s2 & ( for n being Element of NAT holds s2 . n <= b ) ) by Th79;
A4: a #Q s1 is convergent by A1, A2, Th82;
A5: a #Q s2 is convergent by A1, A3, Th82;

now

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

end;

then lim (a #Q s1) >= lim (a #Q s2) by A4, A5, SEQ_2:32;
then a #R c >= lim (a #Q s2) by A1, A2, A4, Def8;
hence a #R c >= a #R b by A1, A3, A5, Def8; :: thesis: verum