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

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;