theorem Th59: :: CARDFIL4:72

for Rseq being Function of [:NAT,NAT:],REAL st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} holds
ex x being Real st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x}