:: deftheorem defines P-convergent_to_+infty DBLSEQ_3:def 2 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_+infty iff for g being Real st 0 < g holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= Eseq . (n,m) );