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

now

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

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

then - 0 < - (seq . n) by XREAL_1:26;
then consider n1 being Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - 0 ) < - (seq . n) by A2, SEQ_2:def 7;
A8: abs ((seq . (n1 + n)) - 0 ) < - (seq . n) by A7, NAT_1:12;
A9: n <= n1 + n by NAT_1:12;
then seq . (n1 + n) < 0 by A3, A6, SEQM_3:14;
then - (seq . (n1 + n)) < - (seq . n) by A8, ABSVALUE:def 1;
then seq . n < seq . (n1 + n) by XREAL_1:26;
hence contradiction by A3, A9, SEQM_3:14; :: 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