:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :
for IT being FinSequence of REAL holds
( IT is non-decreasing iff for n being Nat st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1) );