defpred S₁[ set ] means card (X \ $1) in card X;
set IT = { Y where Y is Subset of X : S₁[Y] } ;
A1: { Y where Y is Subset of X : S₁[Y] } is Subset-Family of X from DOMAIN_1:sch 7();
card (X \ X) = card {} by XBOOLE_1:37
.= 0 ;
then A2: card (X \ X) in card X by ORDINAL3:8;
X c= X ;
then X in { Y where Y is Subset of X : S₁[Y] } by A2;
then reconsider IT = { Y where Y is Subset of X : S₁[Y] } as non empty Subset-Family of X by A1;
A3: for Y1 being Subset of X st Y1 in IT holds
card (X \ Y1) in card X

proof

let Y1 be Subset of X; :: thesis:
assume Y1 in IT ; :: thesis:
then A4: Y1 in { Y where Y is Subset of X : S₁[Y] } ;
thus S₁[Y1] from CARD_FIL:sch 1(A4); :: thesis:

end;

IT is Filter of X

proof

thus not {} in IT :: according to CARD_FIL:def 1 :: thesis:

proof

assume {} in IT ; :: thesis:
then card (X \ {}) in card X by A3;
hence contradiction ; :: thesis:

end;

let Y1, Y2 be Subset of X; :: thesis:
thus ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) :: thesis:

proof

assume ( Y1 in IT & Y2 in IT ) ; :: thesis:
then ( card (X \ Y1) in card X & card (X \ Y2) in card X ) by A3;
then (card (X \ Y1)) +` (card (X \ Y2)) in (card X) +` (card X) by CARD_2:96;
then A5: (card (X \ Y1)) +` (card (X \ Y2)) in card X by CARD_2:75;
card (X \ (Y1 /\ Y2)) = card ((X \ Y1) \/ (X \ Y2)) by XBOOLE_1:54;
then card (X \ (Y1 /\ Y2)) in card X by A5, CARD_2:34, ORDINAL1:12;
hence Y1 /\ Y2 in IT ; :: thesis:

end;

thus ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) :: thesis:

proof

assume ( Y1 in IT & Y1 c= Y2 ) ; :: thesis:
then ( card (X \ Y1) in card X & X \ Y2 c= X \ Y1 ) by A3, XBOOLE_1:34;
then card (X \ Y2) in card X by CARD_1:11, ORDINAL1:12;
hence Y2 in IT ; :: thesis:

end;

end;

hence { Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X ; :: thesis: