theorem Th22: :: CARD_FIL:22

for X being infinite set
for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )