theorem Th2: :: INTEGR24:2

for seq being Real_Sequence st seq is divergent_to+infty holds
( not seq is divergent_to-infty & not seq is convergent )