theorem :: DBLSEQ_2:38

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
for i1, i2, j1, j2 being Nat st i1 <= i2 & j1 <= j2 holds
(Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2)