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 )
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 )
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