for Rseq being Function of [:NAT,NAT:],REAL
for r being Real st Rseq is P-convergent & ( for n, m being Nat holds Rseq . (n,m) >= r ) holds
P-lim Rseq >= r