:: deftheorem defines non-decreasing DBLSEQ_1:def 11 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is non-decreasing iff for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
Rseq . (n1,m1) >= Rseq . (n2,m2) );