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

( 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