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