:: deftheorem defines increasing SEQM_3:def 6 :
for f being Real_Sequence holds
( f is increasing iff for n being Nat holds f . n < f . (n + 1) );