theorem :: CARDFIL2:64

for X being infinite set holds { (X \ A) where A is finite Subset of X : verum } is Filter of X