:: deftheorem defines Frechet_Ideal CARD_FIL:def 11 :
for X being infinite set holds Frechet_Ideal X = dual (Frechet_Filter X);