let seq, seq' be Real_Sequence; :: thesis: ( seq is convergent & seq' is convergent & ( for n being Element of NAT holds seq . n <= seq' . n ) implies lim seq <= lim seq' )
assume that
A1: seq is convergent and
A2: seq' is convergent and
A3: for n being Element of NAT holds seq . n <= seq' . n ; :: thesis: lim seq <= lim seq'
A4: seq' - seq is convergent by A1, A2, Th25;

now

let n be Element of NAT ; :: thesis: 0 <= (seq' - seq) . n
seq . n <= seq' . n by A3;
then A5: (seq . n) - (seq . n) <= (seq' . n) - (seq . n) by XREAL_1:11;
(seq' - seq) . n = (seq' . n) + ((- seq) . n) by SEQ_1:11
.= (seq' . n) + (- (seq . n)) by SEQ_1:14
.= (seq' . n) - (seq . n) ;
hence 0 <= (seq' - seq) . n by A5; :: thesis: verum

end;

then A6: 0 <= lim (seq' - seq) by A4, Th31;
lim (seq' - seq) = (lim seq') - (lim seq) by A1, A2, Th26;
then 0 + (lim seq) <= ((lim seq') - (lim seq)) + (lim seq) by A6, XREAL_1:8;
hence lim seq <= lim seq' ; :: thesis: verum