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

proof

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;

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

proof

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;

Y = {}

proof

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;

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

end;

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