consider Uf being Filter of X such that

A1: Frechet_Filter X c= Uf and

A2: Uf is being_ultrafilter by Th17;

take Uf ; :: thesis: ( not Uf is principal & Uf is being_ultrafilter )

A3: Uf is uniform by A1, Th20;

not Uf is principal

A1: Frechet_Filter X c= Uf and

A2: Uf is being_ultrafilter by Th17;

take Uf ; :: thesis: ( not Uf is principal & Uf is being_ultrafilter )

A3: Uf is uniform by A1, Th20;

not Uf is principal

proof

hence
( not Uf is principal & Uf is being_ultrafilter )
by A2; :: thesis: verum
assume
Uf is principal
; :: thesis: contradiction

then consider Y being Subset of X such that

A4: Y in Uf and

A5: for Z being Subset of X st Z in Uf holds

Y c= Z ;

A6: for x being Element of X holds X \ {x} in Uf

end;then consider Y being Subset of X such that

A4: Y in Uf and

A5: for Z being Subset of X st Z in Uf holds

Y c= Z ;

A6: for x being Element of X holds X \ {x} in Uf

proof

A9:
for x being Element of X holds not x in Y
let x be Element of X; :: thesis: X \ {x} in Uf

A7: card X <> card {x} ;

{x} is finite Subset of X by SUBSET_1:33;

then A8: ( X \ {x} in Uf or {x} in Uf ) by A2;

assume not X \ {x} in Uf ; :: thesis: contradiction

hence contradiction by A3, A8, A7; :: thesis: verum

end;A7: card X <> card {x} ;

{x} is finite Subset of X by SUBSET_1:33;

then A8: ( X \ {x} in Uf or {x} in Uf ) by A2;

assume not X \ {x} in Uf ; :: thesis: contradiction

hence contradiction by A3, A8, A7; :: thesis: verum

proof

Y = {}
let x be Element of X; :: thesis: not x in Y

assume A10: x in Y ; :: thesis: contradiction

Y c= X \ {x} by A5, A6;

then not x in {x} by A10, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;assume A10: x in Y ; :: thesis: contradiction

Y c= X \ {x} by A5, A6;

then not x in {x} by A10, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

proof

hence
contradiction
by A4, Def1; :: thesis: verum
assume
Y <> {}
; :: thesis: contradiction

then ex x being object st x in Y by XBOOLE_0:def 1;

hence contradiction by A9; :: thesis: verum

end;then ex x being object st x in Y by XBOOLE_0:def 1;

hence contradiction by A9; :: thesis: verum