let M be non limit_cardinal Aleph; :: thesis: for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )
given F being Filter of M such that A1: ( F is uniform & F is being_ultrafilter & F is_complete_with M ) ; :: thesis: contradiction
Frechet_Ideal M c= dual F

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in Frechet_Ideal M or X in dual F )
assume A3: X in Frechet_Ideal M ; :: thesis: X in dual F
reconsider X1 = X as Subset of M by A3;
A4: card X1 in card M by A3, Th19;
assume not X in dual F ; :: thesis: contradiction
then X1 in F by A1, Th22;
then card X1 = card M by A1, Def5;
hence contradiction by A4; :: thesis: verum

end;

then consider S being Subset-Family of M such that
A5: card S = M and
A6: for X1 being set st X1 in S holds
not X1 in dual F and
A7: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 by A1, Th12, Th35;
A8: for X1 being set st X1 in S holds
X1 in F

proof

let X1 be set ; :: thesis: ( X1 in S implies X1 in F )
assume A9: X1 in S ; :: thesis: X1 in F
reconsider X2 = X1 as Subset of M by A9;
not X2 in dual F by A6, A9;
hence X1 in F by A1, Th22; :: thesis: verum

end;

not S is finite by A5;
then consider X1 being set such that
A11: X1 in S by XBOOLE_0:def 1;
S \ {X1} <> {}

proof

assume S \ {X1} = {} ; :: thesis: contradiction
then S c= {X1} by XBOOLE_1:37;
hence contradiction by A5; :: thesis: verum

end;

then consider X2 being set such that
A12: X2 in S \ {X1} by XBOOLE_0:def 1;
A13: S \ {X1} is Subset of S ;
not X2 in {X1} by A12, XBOOLE_0:def 5;
then ( X2 in S & X2 <> X1 ) by A12, A13, TARSKI:def 1;
then X1 misses X2 by A7, A11;
then A14: X1 /\ X2 = {} by XBOOLE_0:def 7;
reconsider X1 = X1, X2 = X2 as Subset of M by A11, A12;
( X1 in F & X2 in F ) by A8, A11, A12, A13;
then {} in F by A14, Def1;
hence contradiction by Def1; :: thesis: verum