:: deftheorem defines Frechet_Filter CARD_FIL:def 10 :
for X being infinite set holds Frechet_Filter X = { Y where Y is Subset of X : card (X \ Y) in card X } ;