let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded_below & seq1 is divergent_to-infty implies seq - seq1 is divergent_to+infty )
assume that
A1: seq is bounded_below and
A2: seq1 is divergent_to-infty ; :: thesis: seq - seq1 is divergent_to+infty
(- 1) (#) seq1 is divergent_to+infty by A2, Th41;
hence seq - seq1 is divergent_to+infty by A1, Th36; :: thesis: verum