let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded_above & seq1 is divergent_to+infty implies seq - seq1 is divergent_to-infty )
assume that
A1: seq is bounded_above and
A2: seq1 is divergent_to+infty ; :: thesis: seq - seq1 is divergent_to-infty
(- jj) (#) seq1 is divergent_to-infty by A2, Th13;
hence seq - seq1 is divergent_to-infty by A1, Th12; :: thesis: verum