for seq being Real_Sequence holds
( ( seq is divergent_to+infty implies - seq is divergent_to-infty ) & ( seq is divergent_to-infty implies - seq is divergent_to+infty ) ) by Th13, Th14;