let a, b, c be Real; ( a >= 1 & c >= b implies a #R c >= a #R b )
assume that
A1:
a >= 1
and
A2:
c >= b
; a #R c >= a #R b
consider s1 being Rational_Sequence such that
A3:
s1 is convergent
and
A4:
c = lim s1
and
A5:
for n being Nat holds s1 . n >= c
by Th68;
A6:
a #Q s1 is convergent
by A1, A3, Th69;
consider s2 being Rational_Sequence such that
A7:
s2 is convergent
and
A8:
b = lim s2
and
A9:
for n being Nat holds s2 . n <= b
by Th67;
A10:
a #Q s2 is convergent
by A1, A7, Th69;
then
lim (a #Q s1) >= lim (a #Q s2)
by A6, A10, SEQ_2:18;
then
a #R c >= lim (a #Q s2)
by A1, A3, A4, A6, Def6;
hence
a #R c >= a #R b
by A1, A7, A8, A10, Def6; verum