theorem :: LIMFUNC1:17

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is divergent_to+infty holds
seq - seq1 is divergent_to-infty