let seq be Real_Sequence; :: thesis: ( seq is non-increasing & not seq is bounded_below implies seq is divergent_to-infty )
assume that
A1: seq is non-increasing and
A2: not seq is bounded_below ; :: thesis: seq is divergent_to-infty
let r be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m < r
consider n being Element of NAT such that
A3: seq . n <= r - 1 by A2, SEQ_2:def 4;
take n ; :: thesis: for m being Element of NAT st n <= m holds
seq . m < r
let m be Element of NAT ; :: thesis: ( n <= m implies seq . m < r )
assume n <= m ; :: thesis: seq . m < r
then seq . m <= seq . n by A1, SEQM_3:14;
then seq . m <= r - 1 by A3, XXREAL_0:2;
hence seq . m < r by Lm1; :: thesis: verum