let X be non empty set ; :: thesis: for F being Filter of X ex Uf being Filter of X st

( F c= Uf & Uf is being_ultrafilter )

let F be Filter of X; :: thesis: ex Uf being Filter of X st

( F c= Uf & Uf is being_ultrafilter )

set LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;

A1: F in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;

{ S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } c= Filters X

defpred S_{1}[ set ] means ( F c= $1 & $1 is Filter of X );

for Z being set st Z c= LargerF & Z is c=-linear holds

ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in Z holds

X1 c= Y ) )

A10: Uf1 in LargerF and

A11: for Z being set st Z in LargerF & Z <> Uf1 holds

not Uf1 c= Z by ORDERS_1:65;

reconsider Uf1 = Uf1 as Element of LargerF by A10;

reconsider Uf = Uf1 as Filter of X by Th15;

take Uf ; :: thesis: ( F c= Uf & Uf is being_ultrafilter )

A12: Uf in { S where S is Subset-Family of X : S_{1}[S] }
;

A13: S_{1}[Uf]
from CARD_FIL:sch 1(A12);

hence F c= Uf ; :: thesis: Uf is being_ultrafilter

thus Uf is being_ultrafilter :: thesis: verum

( F c= Uf & Uf is being_ultrafilter )

let F be Filter of X; :: thesis: ex Uf being Filter of X st

( F c= Uf & Uf is being_ultrafilter )

set LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;

A1: F in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;

{ S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } c= Filters X

proof

then reconsider LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } as non empty Subset of (Filters X) by A1;
defpred S_{1}[ set ] means ( F c= $1 & $1 is Filter of X );

let F2 be object ; :: according to TARSKI:def 3 :: thesis: ( not F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } or F2 in Filters X )

reconsider FF = F2 as set by TARSKI:1;

assume F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ; :: thesis: F2 in Filters X

then A2: FF in { S where S is Subset-Family of X : S_{1}[S] }
;

S_{1}[FF]
from CARD_FIL:sch 1(A2);

hence F2 in Filters X ; :: thesis: verum

end;let F2 be object ; :: according to TARSKI:def 3 :: thesis: ( not F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } or F2 in Filters X )

reconsider FF = F2 as set by TARSKI:1;

assume F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ; :: thesis: F2 in Filters X

then A2: FF in { S where S is Subset-Family of X : S

S

hence F2 in Filters X ; :: thesis: verum

defpred S

for Z being set st Z c= LargerF & Z is c=-linear holds

ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in Z holds

X1 c= Y ) )

proof

then consider Uf1 being set such that
let X1 be set ; :: thesis: ( X1 c= LargerF & X1 is c=-linear implies ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) ) )

assume that

A3: X1 c= LargerF and

A4: X1 is c=-linear ; :: thesis: ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) )

end;( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) ) )

assume that

A3: X1 c= LargerF and

A4: X1 is c=-linear ; :: thesis: ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) )

per cases
( X1 = {} or not X1 is empty )
;

end;

suppose A5:
X1 = {}
; :: thesis: ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) )

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) )

take
F
; :: thesis: ( F in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= F ) )

thus ( F in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= F ) ) by A5; :: thesis: verum

end;X1 c= F ) )

thus ( F in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= F ) ) by A5; :: thesis: verum

suppose
not X1 is empty
; :: thesis: ex Y being set st

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) )

( Y in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= Y ) )

then reconsider X2 = X1 as non empty Subset of (Filters X) by A3, XBOOLE_1:1;

A6: F c= union X2

then union X2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } by A6;

then reconsider MF = union X2 as Element of LargerF ;

take MF ; :: thesis: ( MF in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= MF ) )

thus ( MF in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= MF ) ) by ZFMISC_1:74; :: thesis: verum

end;A6: F c= union X2

proof

union X2 is Filter of X
by A4, Th16;
defpred S_{2}[ set ] means ( F c= $1 & $1 is Filter of X );

consider F1 being object such that

A7: F1 in X2 by XBOOLE_0:def 1;

reconsider F1 = F1 as set by TARSKI:1;

A8: F1 in { S where S is Subset-Family of X : S_{2}[S] }
by A3, A7;

A9: S_{2}[F1]
from CARD_FIL:sch 1(A8);

F1 c= union X2 by A7, ZFMISC_1:74;

hence F c= union X2 by A9; :: thesis: verum

end;consider F1 being object such that

A7: F1 in X2 by XBOOLE_0:def 1;

reconsider F1 = F1 as set by TARSKI:1;

A8: F1 in { S where S is Subset-Family of X : S

A9: S

F1 c= union X2 by A7, ZFMISC_1:74;

hence F c= union X2 by A9; :: thesis: verum

then union X2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } by A6;

then reconsider MF = union X2 as Element of LargerF ;

take MF ; :: thesis: ( MF in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= MF ) )

thus ( MF in LargerF & ( for X1 being set st X1 in X1 holds

X1 c= MF ) ) by ZFMISC_1:74; :: thesis: verum

A10: Uf1 in LargerF and

A11: for Z being set st Z in LargerF & Z <> Uf1 holds

not Uf1 c= Z by ORDERS_1:65;

reconsider Uf1 = Uf1 as Element of LargerF by A10;

reconsider Uf = Uf1 as Filter of X by Th15;

take Uf ; :: thesis: ( F c= Uf & Uf is being_ultrafilter )

A12: Uf in { S where S is Subset-Family of X : S

A13: S

hence F c= Uf ; :: thesis: Uf is being_ultrafilter

thus Uf is being_ultrafilter :: thesis: verum

proof

let Z be Subset of X; :: according to CARD_FIL:def 7 :: thesis: ( Z in Uf or X \ Z in Uf )

end;per cases
( Z in Uf or not Z in Uf )
;

end;

suppose A14:
not Z in Uf
; :: thesis: ( Z in Uf or X \ Z in Uf )

X \ Z in Uf

end;proof

hence
( Z in Uf or X \ Z in Uf )
; :: thesis: verum
assume A15:
not X \ Z in Uf
; :: thesis: contradiction

A16: for Y1 being Subset of X st Y1 in Uf holds

Y1 meets Z

A19: Z in Extend_Filter (Uf,Z) by A16, Th14;

A20: Uf c= Extend_Filter (Uf,Z) by A16, Th14;

then F c= Extend_Filter (Uf,Z) by A13;

then Extend_Filter (Uf,Z) in LargerF by A18;

hence contradiction by A11, A14, A20, A19; :: thesis: verum

end;A16: for Y1 being Subset of X st Y1 in Uf holds

Y1 meets Z

proof

then A18:
Extend_Filter (Uf,Z) is Filter of X
by Th14;
let Y1 be Subset of X; :: thesis: ( Y1 in Uf implies Y1 meets Z )

assume A17: Y1 in Uf ; :: thesis: Y1 meets Z

assume Y1 misses Z ; :: thesis: contradiction

then Y1 = Y1 \ Z by XBOOLE_1:83;

then Y1 c= X \ Z by XBOOLE_1:33;

hence contradiction by A15, A17, Def1; :: thesis: verum

end;assume A17: Y1 in Uf ; :: thesis: Y1 meets Z

assume Y1 misses Z ; :: thesis: contradiction

then Y1 = Y1 \ Z by XBOOLE_1:83;

then Y1 c= X \ Z by XBOOLE_1:33;

hence contradiction by A15, A17, Def1; :: thesis: verum

A19: Z in Extend_Filter (Uf,Z) by A16, Th14;

A20: Uf c= Extend_Filter (Uf,Z) by A16, Th14;

then F c= Extend_Filter (Uf,Z) by A13;

then Extend_Filter (Uf,Z) in LargerF by A18;

hence contradiction by A11, A14, A20, A19; :: thesis: verum