let X be infinite set ; :: thesis:
set FF = { (X \ A) where A is finite Subset of X : verum } ;

let x be object ; :: thesis:
assume x in { (X \ A) where A is finite Subset of X : verum } ; :: thesis:
then consider a1 being finite Subset of X such that
A1: x = X \ a1 ;
thus x in bool X by A1; :: thesis:

end;

then { (X \ A) where A is finite Subset of X : verum } c= bool X ;
then reconsider FF = { (X \ A) where A is finite Subset of X : verum } as non empty Subset-Family of X by Th28;
A2: not {} in FF

assume {} in FF ; :: thesis:
then consider a being finite Subset of X such that
A3: {} = X \ a ;
X c= a by A3, XBOOLE_1:37;
hence contradiction ; :: thesis:

end;

A4: for Y1, Y2 being Subset of X st Y1 in FF & Y2 in FF holds
Y1 /\ Y2 in FF

let Y1, Y2 be Subset of X; :: thesis:
assume that
A5: Y1 in FF and
A6: Y2 in FF ; :: thesis:
consider a1 being finite Subset of X such that
A7: Y1 = X \ a1 by A5;
consider a2 being finite Subset of X such that
A8: Y2 = X \ a2 by A6;
Y1 /\ Y2 = X \ (a1 \/ a2) by A7, A8, XBOOLE_1:53;
hence Y1 /\ Y2 in FF ; :: thesis:

end;

for Y1, Y2 being Subset of X st Y1 in FF & Y1 c= Y2 holds
Y2 in FF

let Y1, Y2 be Subset of X; :: thesis:
assume that
A9: Y1 in FF and
A10: Y1 c= Y2 ; :: thesis:
consider a1 being finite Subset of X such that
A11: Y1 = X \ a1 by A9;
X \ Y2 c= X \ (X \ a1) by A10, A11, XBOOLE_1:34;
then A12: X \ Y2 c= X /\ a1 by XBOOLE_1:48;
( X \ (X \ Y2) = X /\ Y2 & X /\ Y2 c= Y2 ) by XBOOLE_1:17, XBOOLE_1:48;
then X \ (X \ Y2) = Y2 by XBOOLE_1:28;
hence Y2 in FF by A12; :: thesis:

end;

hence { (X \ A) where A is finite Subset of X : verum } is Filter of X by A2, A4, CARD_FIL:def 1; :: thesis: