:: deftheorem defines non-decreasing SEQM_3:def 8 :
for f being Real_Sequence holds
( f is non-decreasing iff for n being Nat holds f . n <= f . (n + 1) );