let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for r being Real st Rseq is P-convergent & ( for n, m being Nat holds Rseq . (n,m) >= r ) holds
P-lim Rseq >= r
let r be Real; :: thesis: ( Rseq is P-convergent & ( for n, m being Nat holds Rseq . (n,m) >= r ) implies P-lim Rseq >= r )
assume a1: Rseq is P-convergent ; :: thesis: ( ex n, m being Nat st not Rseq . (n,m) >= r or P-lim Rseq >= r )
assume a2: for n, m being Nat holds Rseq . (n,m) >= r ; :: thesis: P-lim Rseq >= r
assume not P-lim Rseq >= r ; :: thesis: contradiction
then r - (P-lim Rseq) > 0 by XREAL_1:50;
then consider N being Nat such that
a3: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq)).| < r - (P-lim Rseq) by a1, def6;
|.((Rseq . (N,N)) - (P-lim Rseq)).| < r - (P-lim Rseq) by a3;
then (P-lim Rseq) + (r - (P-lim Rseq)) > Rseq . (N,N) by RINFSUP1:1;
hence contradiction by a2; :: thesis: verum