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

now :: thesis: for x being object st x in { (X \ A) where A is finite Subset of X : verum } holds
x in bool X

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

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

proof

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

end;

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

proof

let Y1, Y2 be Subset of X; :: thesis: ( Y1 in FF & Y2 in FF implies Y1 /\ Y2 in FF )
assume that
A5: Y1 in FF and
A6: Y2 in FF ; :: thesis: Y1 /\ Y2 in FF
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: verum

end;

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

proof

let Y1, Y2 be Subset of X; :: thesis: ( Y1 in FF & Y1 c= Y2 implies Y2 in FF )
assume that
A9: Y1 in FF and
A10: Y1 c= Y2 ; :: thesis: Y2 in FF
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: verum

end;

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