let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent & ( for n being Nat holds seq . n <= seq9 . n ) implies lim seq <= lim seq9 )
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n being Nat holds seq . n <= seq9 . n ; :: thesis: lim seq <= lim seq9

now :: thesis: for n being Nat holds 0 <= (seq9 - seq) . n

let n be Nat; :: thesis: 0 <= (seq9 - seq) . n
seq . n <= seq9 . n by A3;
then A4: (seq . n) - (seq . n) <= (seq9 . n) - (seq . n) by XREAL_1:9;
(seq9 - seq) . n = (seq9 . n) + ((- seq) . n) by SEQ_1:7
.= (seq9 . n) + (- (seq . n)) by SEQ_1:10
.= (seq9 . n) - (seq . n) ;
hence 0 <= (seq9 - seq) . n by A4; :: thesis: verum

end;

then A5: 0 <= lim (seq9 - seq) by A1, A2, Th17;
lim (seq9 - seq) = (lim seq9) - (lim seq) by A1, A2, Th12;
then 0 + (lim seq) <= ((lim seq9) - (lim seq)) + (lim seq) by A5, XREAL_1:6;
hence lim seq <= lim seq9 ; :: thesis: verum