let a, b, c be Real; :: thesis: ( a >= 1 & c >= b implies a #R c >= a #R b )

assume that

A1: a >= 1 and

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

assume that

A1: a >= 1 and

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

now :: thesis: for n being Nat holds (a #Q s1) . n >= (a #Q s2) . n

then
lim (a #Q s1) >= lim (a #Q s2)
by A6, A10, SEQ_2:18;let n be Nat; :: thesis: (a #Q s1) . n >= (a #Q s2) . n

s1 . n >= c by A5;

then A11: s1 . n >= b by A2, XXREAL_0:2;

s2 . n <= b by A9;

then s1 . n >= s2 . n by A11, XXREAL_0:2;

then a #Q (s1 . n) >= a #Q (s2 . n) by A1, Th63;

then a #Q (s1 . n) >= (a #Q s2) . n by Def5;

hence (a #Q s1) . n >= (a #Q s2) . n by Def5; :: thesis: verum

end;s1 . n >= c by A5;

then A11: s1 . n >= b by A2, XXREAL_0:2;

s2 . n <= b by A9;

then s1 . n >= s2 . n by A11, XXREAL_0:2;

then a #Q (s1 . n) >= a #Q (s2 . n) by A1, Th63;

then a #Q (s1 . n) >= (a #Q s2) . n by Def5;

hence (a #Q s1) . n >= (a #Q s2) . n by Def5; :: thesis: verum

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; :: thesis: verum