theorem Th3: :: INTEGR24:3

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