theorem Th60: :: CARDFIL4:73

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds
P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))