theorem :: DBLSEQ_1:15

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds
P-lim Rseq1 <= P-lim Rseq2