:: deftheorem defines monotone SEQM_3:def 5 :
for seq being Real_Sequence holds
( seq is monotone iff ( seq is non-decreasing or seq is non-increasing ) );