theorem :: CARDFIL2:56

base_of_frechet_filter is basis of (Frechet_Filter NAT) by Th27;