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

proof

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 by Def6;
A6: for x being Element of X holds X \ {x} in Uf

proof

let x be Element of X; :: thesis: X \ {x} in Uf
assume A7: not X \ {x} in Uf ; :: thesis: contradiction
{x} is finite Subset of X by SUBSET_1:55;
then A8: ( X \ {x} in Uf or {x} in Uf ) by A2, Def7;
card X <> card {x} ;
hence contradiction by A3, A7, A8, Def5; :: thesis: verum

end;

A9: for x being Element of X holds not x in Y

proof

let x be Element of X; :: thesis: not x in Y
A10: Y c= X \ {x} by A5, A6;
assume x in Y ; :: thesis: contradiction
then not x in {x} by A10, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

Y = {}

proof

assume Y <> {} ; :: thesis: contradiction
then consider x being set such that
A11: x in Y by XBOOLE_0:def 1;
thus contradiction by A9, A11; :: thesis: verum

end;

hence contradiction by A4, Def1; :: thesis: verum

end;

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