let X be infinite set ; :: thesis: for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds

Frechet_Filter X c= Uf

let Uf be Filter of X; :: thesis: ( Uf is uniform & Uf is being_ultrafilter implies Frechet_Filter X c= Uf )

assume A1: ( Uf is uniform & Uf is being_ultrafilter ) ; :: thesis: Frechet_Filter X c= Uf

thus Frechet_Filter X c= Uf :: thesis: verum

Frechet_Filter X c= Uf

let Uf be Filter of X; :: thesis: ( Uf is uniform & Uf is being_ultrafilter implies Frechet_Filter X c= Uf )

assume A1: ( Uf is uniform & Uf is being_ultrafilter ) ; :: thesis: Frechet_Filter X c= Uf

thus Frechet_Filter X c= Uf :: thesis: verum

proof

let Y be object ; :: according to TARSKI:def 3 :: thesis: ( not Y in Frechet_Filter X or Y in Uf )

reconsider YY = Y as set by TARSKI:1;

assume A2: Y in Frechet_Filter X ; :: thesis: Y in Uf

then card (X \ YY) in card X by Th18;

then card (X \ YY) <> card X ;

then not X \ YY in Uf by A1;

hence Y in Uf by A1, A2; :: thesis: verum

end;reconsider YY = Y as set by TARSKI:1;

assume A2: Y in Frechet_Filter X ; :: thesis: Y in Uf

then card (X \ YY) in card X by Th18;

then card (X \ YY) <> card X ;

then not X \ YY in Uf by A1;

hence Y in Uf by A1, A2; :: thesis: verum