:: deftheorem defines decreasing SEQM_3:def 7 :
for f being Real_Sequence holds
( f is decreasing iff for n being Nat holds f . n > f . (n + 1) );