let seq be Real_Sequence; :: thesis: ( seq is convergent & ( for n being Element of NAT holds 0 <= seq . n ) implies 0 <= lim seq )
assume that
A1: seq is convergent and
A2: for n being Element of NAT holds 0 <= seq . n and
A3: not 0 <= lim seq ; :: thesis: contradiction
0 < - (lim seq) by A3, XREAL_1:58;
then consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < - (lim seq) by A1, Def7;
abs ((seq . n1) - (lim seq)) <= - (lim seq) by A4;
then (seq . n1) - (lim seq) <= - (lim seq) by ABSVALUE:5;
then A5: ((seq . n1) - (lim seq)) + (lim seq) <= (- (lim seq)) + (lim seq) by XREAL_1:6;

now

assume seq . n1 = 0 ; :: thesis: contradiction
then abs ((seq . n1) - (lim seq)) = - (lim seq) by A3, ABSVALUE:def 1;
hence contradiction by A4; :: thesis: verum

end;

hence contradiction by A2, A5; :: thesis: verum