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