theorem Th64: :: CARDFIL4:78

0 in lim_filter ((# dblseq_ex_1),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by Th63, Th58;