theorem :: CARDFIL4:80

lim_filter ((# dblseq_ex_1),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) by Th63, Th58, Th65;