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
A4: 0 < - (lim seq) by A3, XREAL_1:60;
then consider n1 being Element of NAT such that
A5: 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) & abs ((seq . n1) - (lim seq)) <> - (lim seq) ) by A5;
then (seq . n1) - (lim seq) <= - (lim seq) by ABSVALUE:12;
then A6: ((seq . n1) - (lim seq)) + (lim seq) <= (- (lim seq)) + (lim seq) by XREAL_1:8;

now

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

end;

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