let seq be Real_Sequence; :: thesis: ( seq is convergent & ( for n being Nat holds 0 <= seq . n ) implies 0 <= lim seq )
assume that
A1: seq is convergent and
A2: for n being Nat holds 0 <= seq . n and
A3: not 0 <= lim seq ; :: thesis: contradiction
0 < - (lim seq) by A3;
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < - (lim seq) by A1, Def6;
|.((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 :: thesis: not seq . n1 = 0

assume seq . n1 = 0 ; :: thesis: contradiction
then |.((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