let X be infinite set ; :: thesis: for F being Filter of X st Frechet_Filter X c= F holds
F is uniform
let F be Filter of X; :: thesis: ( Frechet_Filter X c= F implies F is uniform )
assume A1: Frechet_Filter X c= F ; :: thesis: F is uniform
let Y be Subset of X; :: according to CARD_FIL:def 5 :: thesis: ( Y in F implies card Y = card X )
assume Y in F ; :: thesis: card Y = card X
then not X \ Y in Frechet_Filter X by A1, Th6;
then A2: not card (X \ (X \ Y)) in card X ;
A3: card Y c= card X by CARD_1:11;
X \ (X \ Y) = X /\ Y by XBOOLE_1:48
.= Y by XBOOLE_1:28 ;
then card X c= card Y by A2, CARD_1:4;
hence card Y = card X by A3; :: thesis: verum