:: deftheorem defines non-increasing SEQM_3:def 4 :
for f being NAT -defined real-valued Function holds
( f is non-increasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds
f . m >= f . n );