:: deftheorem defines non-increasing SEQM_3:def 9 :
for f being Real_Sequence holds
( f is non-increasing iff for n being Nat holds f . n >= f . (n + 1) );