theorem Th96: :: DBLSEQ_3:96

for f being Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2) ) holds
( f is P-convergent & P-lim f = sup (rng f) )