theorem Th18: :: CARD_FIL:18

for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Filter X iff card (X \ Y) in card X )