reconsider FX = {X} as Filter of X by CARD_FIL:4;
FX in { F where F is Filter of X : verum } ;
hence { F where F is Filter of X : verum } is non empty set ; :: thesis: verum