let F be Filter of X; :: thesis: ( F is uniform & F is being_ultrafilter implies not F is principal )
assume A1: ( F is uniform & F is being_ultrafilter ) ; :: thesis: not F is principal
assume F is principal ; :: thesis: contradiction
then consider Y being Subset of X such that
A2: Y in F and
A3: for Z being Subset of X st Z in F holds
Y c= Z ;
Y = {}
proof
assume Y <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in Y by XBOOLE_0:def 1;
A5: for Z being Subset of X st Z in F holds
x in Z
proof
let Z be Subset of X; :: thesis: ( Z in F implies x in Z )
assume Z in F ; :: thesis: x in Z
then Y c= Z by A3;
hence x in Z by A4; :: thesis: verum
end;
card {x} in card X by CARD_3:86;
then A6: not {x} in F by A1;
{x} is Subset of X by A4, SUBSET_1:33;
then X \ {x} in F by A1, A6;
then x in X \ {x} by A5;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
hence contradiction by A2, Def1; :: thesis: verum