theorem Th37: :: CARDFIL4:45

<.(Frechet_Filter NAT),(Frechet_Filter NAT).) is_filter-finer_than Frechet_Filter [:NAT,NAT:]