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