:: deftheorem Def3 defines non-increasing RFINSEQ:def 3 :
for IT being real-valued FinSequence holds
( IT is non-increasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) );