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 = {}

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

hence
contradiction
by A2, Def1; :: thesis: verum
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

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;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

card {x} in card X
by CARD_3:86;
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;assume Z in F ; :: thesis: x in Z

then Y c= Z by A3;

hence x in Z by A4; :: thesis: verum

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