let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing implies seq " is divergent_to-infty )
assume A1: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing ) ; :: thesis: seq " is divergent_to-infty
then for n being Element of NAT st 0 <= n holds
seq . n < 0 by Th27;
hence seq " is divergent_to-infty by A1, Th63; :: thesis: verum