base_of_frechet_filter is basis of (Frechet_Filter NAT) by Th27;