let seq be Real_Sequence; :: thesis: ( seq is convergent & ( for n being Element of NAT holds seq . n <= 0 ) implies lim seq <= 0 )
assume that
A1: seq is convergent and
A2: for n being Element of NAT holds seq . n <= 0 ; :: thesis: lim seq <= 0
set seq1 = - seq;

A3: now

let n be Element of NAT ; :: thesis: - 0 <= (- seq) . n
( (- seq) . n = - (seq . n) & seq . n <= 0 ) by A2, SEQ_1:14;
hence - 0 <= (- seq) . n by XREAL_1:26; :: thesis: verum

end;

- seq is convergent by A1, SEQ_2:23;
then 0 <= lim (- seq) by A3, SEQ_2:31;
then - 0 <= - (lim seq) by A1, SEQ_2:24;
hence lim seq <= 0 by XREAL_1:26; :: thesis: verum