theorem :: CARDFIL4:40

[:base_of_frechet_filter,base_of_frechet_filter:] is filter_base of [:NAT,NAT:] ;