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