let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq1 is P-convergent & Rseq2 is P-convergent & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) implies P-lim Rseq1 <= P-lim Rseq2 )
assume a1: ( Rseq1 is P-convergent & Rseq2 is P-convergent ) ; :: thesis: ( ex n, m being Nat st not Rseq1 . (n,m) <= Rseq2 . (n,m) or P-lim Rseq1 <= P-lim Rseq2 )
assume a2: for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ; :: thesis: P-lim Rseq1 <= P-lim Rseq2
a3: ( Rseq2 - Rseq1 is P-convergent & P-lim (Rseq2 - Rseq1) = (P-lim Rseq2) - (P-lim Rseq1) ) by a1, th54b;
now :: thesis: for n, m being Nat holds (Rseq2 - Rseq1) . (n,m) >= 0
let n, m be Nat; :: thesis: (Rseq2 - Rseq1) . (n,m) >= 0
(Rseq2 - Rseq1) . (n,m) = (Rseq2 . (n,m)) - (Rseq1 . (n,m)) by lmADD;
hence (Rseq2 - Rseq1) . (n,m) >= 0 by a2, XREAL_1:48; :: thesis: verum
end;
hence P-lim Rseq1 <= P-lim Rseq2 by a3, th55b, XREAL_1:49; :: thesis: verum