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 ) and
A2: F is_complete_with M ; :: thesis: contradiction
Frechet_Ideal M c= dual F
proof
let X be object ; :: 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;
assume not X in dual F ; :: thesis: contradiction
then X1 in F by A1, Th22;
then A4: card X1 = card M by A1;
card X1 in card M by A3, Th19;
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 A2, Th12, Th35;
S is infinite by A5;
then consider X1 being object such that
A8: 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 object such that
A9: X2 in S \ {X1} by XBOOLE_0:def 1;
A10: S \ {X1} is Subset of S ;
reconsider X1 = X1, X2 = X2 as set by TARSKI:1;
not X2 in {X1} by A9, XBOOLE_0:def 5;
then X2 <> X1 by TARSKI:def 1;
then X1 misses X2 by A7, A8, A9, A10;
then A11: X1 /\ X2 = {} ;
reconsider X1 = X1, X2 = X2 as Subset of M by A8, A9;
A12: for X1 being set st X1 in S holds
X1 in F by A1, A6, Th22;
then A13: X1 in F by A8;
X2 in F by A12, A9, A10;
then {} in F by A11, A13, Def1;
hence contradiction by Def1; :: thesis: verum