let X be denumerable set ; :: thesis: Frechet_Filter X = { (X \ A) where A is finite Subset of X : verum }
A1: card X = omega by CARD_3:def 15;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (X \ A) where A is finite Subset of X : verum } c= Frechet_Filter X
let x be object ; :: thesis: ( x in Frechet_Filter X implies x in { (X \ A) where A is finite Subset of X : verum } )
assume A2: x in Frechet_Filter X ; :: thesis: x in { (X \ A) where A is finite Subset of X : verum }
reconsider x0 = x as Subset of X by A2;
card (X \ x0) in card X by A2, CARD_FIL:18;
then A3: X \ x0 is finite Subset of X by A1;
( X \ (X \ x0) = X /\ x0 & X /\ x0 c= X ) by XBOOLE_1:48;
then X \ (X \ x0) = x0 by XBOOLE_1:28;
hence x in { (X \ A) where A is finite Subset of X : verum } by A3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (X \ A) where A is finite Subset of X : verum } or x in Frechet_Filter X )
assume A4: x in { (X \ A) where A is finite Subset of X : verum } ; :: thesis: x in Frechet_Filter X
consider a0 being finite Subset of X such that
A5: x = X \ a0 by A4;
reconsider x0 = x as Subset of X by A5;
( X \ (X \ a0) = X /\ a0 & X /\ a0 c= X ) by XBOOLE_1:48;
then card (X \ x0) = card a0 by A5, XBOOLE_1:28;
hence x in Frechet_Filter X by A1; :: thesis: verum