let X be non empty set ; :: thesis: for S being set holds
( S in Filters X iff S is Filter of X )
let S be set ; :: thesis: ( S in Filters X iff S is Filter of X )
thus ( S in Filters X implies S is Filter of X ) :: thesis: ( S is Filter of X implies S in Filters X )

proof

defpred S₁[ set ] means $1 is Filter of X;
assume S in Filters X ; :: thesis: S is Filter of X
then A1: S in { S1 where S1 is Subset-Family of X : S₁[S1] } ;
thus S₁[S] from CARD_FIL:sch 1(A1); :: thesis: verum

end;

assume S is Filter of X ; :: thesis: S in Filters X
hence S in Filters X ; :: thesis: verum