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 )
proof
defpred S1[ 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 : S1[Y1] } ;
thus S1[Y] from CARD_FIL:sch 1(A1); :: thesis: verum
end;
thus ( card (X \ Y) in card X implies Y in Frechet_Filter X ) ; :: thesis: verum