let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing implies seq " is divergent_to+infty )
assume that
A1: seq is non-zero and
A2: ( seq is convergent & lim seq = 0 ) and
A3: seq is non-increasing ; :: thesis: seq " is divergent_to+infty
for n being Nat st 0 <= n holds
0 < seq . n by A1, A2, A3, Th3;
hence seq " is divergent_to+infty by A2, Th35; :: thesis: verum