let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing implies for n being Element of NAT holds seq . n < 0 )
assume that
A1: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing ) and
A2: not for n being Element of NAT holds seq . n < 0 ; :: thesis: contradiction
consider n being Element of NAT such that
A3: not seq . n < 0 by A2;

now

per cases ( 0 < seq . n or seq . n = 0 ) by A3;

suppose A4: 0 < seq . n ; :: thesis: contradiction

then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - 0 ) < seq . n by A1, SEQ_2:def 7;
A6: abs ((seq . (n1 + n)) - 0 ) < seq . n by A5, NAT_1:12;
A7: n <= n1 + n by NAT_1:12;
seq . (n1 + n) < seq . n by A4, A6, ABSVALUE:def 1;
hence contradiction by A1, A7, SEQM_3:12; :: thesis: verum

end;

suppose seq . n = 0 ; :: thesis: contradiction

hence contradiction by A1, SEQ_1:7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum