theorem :: LIMFUNC1:33

for seq being Real_Sequence holds
( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )