:: deftheorem defines base_of_frechet_filter CARDFIL2:def 18 :
base_of_frechet_filter = # (Tails OrderedNAT);