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