let X be infinite set ; :: thesis: for Y being Subset of X holds
( Y in Frechet_Ideal X iff card Y in card X )
let Y be Subset of X; :: thesis: ( Y in Frechet_Ideal X iff card Y in card X )
( Y in Frechet_Ideal X iff Y ` in Frechet_Filter X ) by SETFAM_1:def 7;
then ( Y in Frechet_Ideal X iff card ((Y `) `) in card X ) by Th18;
hence ( Y in Frechet_Ideal X iff card Y in card X ) ; :: thesis: verum