let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty implies - seq is divergent_to-infty ) & ( seq is divergent_to-infty implies - seq is divergent_to+infty ) )
A1: (- 1) (#) seq = - seq ;
hence ( seq is divergent_to+infty implies - seq is divergent_to-infty ) by Th40; :: thesis: ( seq is divergent_to-infty implies - seq is divergent_to+infty )
assume seq is divergent_to-infty ; :: thesis: - seq is divergent_to+infty
hence - seq is divergent_to+infty by A1, Th41; :: thesis: verum