theorem :: CARDFIL2:5

for X being non empty set
for A being non empty Subset of X holds { B where B is Subset of X : A c= B } is Filter of X