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 S1[ 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 : S1[S1] } ;
thus S1[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