let X be infinite set ; :: thesis: for Y being Subset of X holds

( Y in Frechet_Filter X iff card (X \ Y) in card X )

let Y be Subset of X; :: thesis: ( Y in Frechet_Filter X iff card (X \ Y) in card X )

thus ( Y in Frechet_Filter X implies card (X \ Y) in card X ) :: thesis: ( card (X \ Y) in card X implies Y in Frechet_Filter X )

( Y in Frechet_Filter X iff card (X \ Y) in card X )

let Y be Subset of X; :: thesis: ( Y in Frechet_Filter X iff card (X \ Y) in card X )

thus ( Y in Frechet_Filter X implies card (X \ Y) in card X ) :: thesis: ( card (X \ Y) in card X implies Y in Frechet_Filter X )

proof

thus
( card (X \ Y) in card X implies Y in Frechet_Filter X )
; :: thesis: verum
defpred S_{1}[ set ] means card (X \ $1) in card X;

assume Y in Frechet_Filter X ; :: thesis: card (X \ Y) in card X

then A1: Y in { Y1 where Y1 is Subset of X : S_{1}[Y1] }
;

thus S_{1}[Y]
from CARD_FIL:sch 1(A1); :: thesis: verum

end;assume Y in Frechet_Filter X ; :: thesis: card (X \ Y) in card X

then A1: Y in { Y1 where Y1 is Subset of X : S

thus S