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

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