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

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

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

( 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

then consider S being Subset-Family of M such that
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;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

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

then consider X2 being object such that
assume
S \ {X1} = {}
; :: thesis: contradiction

then S c= {X1} by XBOOLE_1:37;

hence contradiction by A5; :: thesis: verum

end;then S c= {X1} by XBOOLE_1:37;

hence contradiction by A5; :: thesis: verum

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