let seq be Real_Sequence; :: thesis: ( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )
assume A1: seq is monotone ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

now :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

per cases ( seq is non-decreasing or seq is non-increasing ) by A1, SEQM_3:def 5;

suppose A2: seq is non-decreasing ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

now :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

per cases ( seq is bounded_above or not seq is bounded_above ) ;

suppose seq is bounded_above ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) by A2; :: thesis: verum

end;

suppose not seq is bounded_above ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) by A2, Th29; :: thesis: verum

end;

end;

end;

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: verum

end;

suppose A3: seq is non-increasing ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

now :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

per cases ( seq is bounded_below or not seq is bounded_below ) ;

suppose seq is bounded_below ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) by A3; :: thesis: verum

end;

suppose not seq is bounded_below ; :: thesis: ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) by A3, Th30; :: thesis: verum

end;

end;

end;

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: verum

end;

end;

end;

hence ( seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: verum