theorem Th24: :: CARDFIL2:51

for X being denumerable set holds Frechet_Filter X = { (X \ A) where A is finite Subset of X : verum }