let X be set ; :: thesis: for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Finite_Subset of X st ultraset BL = union Y
let BL be non trivial B_Lattice; :: thesis: ( ultraset BL = union X & X is Subset of (StoneR BL) implies ex Y being Finite_Subset of X st ultraset BL = union Y )
assume that
A1: ultraset BL = union X and
A2: X is Subset of (StoneR BL) ; :: thesis: ex Y being Finite_Subset of X st ultraset BL = union Y
assume A3: for Y being Finite_Subset of X holds not ultraset BL = union Y ; :: thesis: contradiction
consider Y being Finite_Subset of X such that
A4: not Y is empty by A1, Th32, ZFMISC_1:2;
A5: Y c= X by FINSUB_1:def 5;
then A6: Y c= StoneR BL by A2, XBOOLE_1:1;
consider x being Element of Y;
A7: x in X by A4, A5, TARSKI:def 3;
x in StoneR BL by A4, A6, TARSKI:def 3;
then consider b being Element of BL such that
A8: x = (UFilter BL) . b by Th26;
set CY = { (a `) where a is Element of BL : (UFilter BL) . a in X } ;
consider c being Element of BL such that
A9: c = b ` ;
A10: c in { (a `) where a is Element of BL : (UFilter BL) . a in X } by A7, A8, A9;
{ (a `) where a is Element of BL : (UFilter BL) . a in X } c= the carrier of BL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a `) where a is Element of BL : (UFilter BL) . a in X } or x in the carrier of BL )
assume x in { (a `) where a is Element of BL : (UFilter BL) . a in X } ; :: thesis: x in the carrier of BL
then ex b being Element of BL st
( x = b ` & (UFilter BL) . b in X ) ;
hence x in the carrier of BL ; :: thesis: verum

end;

then reconsider CY = { (a `) where a is Element of BL : (UFilter BL) . a in X } as non empty Subset of BL by A10;
set H = <.CY.);
for B being non empty Finite_Subset of the carrier of BL st B c= CY holds
FinMeet B <> Bottom BL

proof

let B be non empty Finite_Subset of the carrier of BL; :: thesis: ( B c= CY implies FinMeet B <> Bottom BL )
assume that
A11: B c= CY and
A12: FinMeet B = Bottom BL ; :: thesis: contradiction
A13: B is Subset of BL by FINSUB_1:32;
A14: dom (UFilter BL) = the carrier of BL by FUNCT_2:def 1;
(UFilter BL) .: B c= rng (UFilter BL) by RELAT_1:144;
then reconsider D = (UFilter BL) .: B as non empty Subset-Family of (ultraset BL) by A13, A14, XBOOLE_1:1;

A15: now

consider x being Element of (UFilter BL) . (Bottom BL);
assume {} (ultraset BL) <> (UFilter BL) . (Bottom BL) ; :: thesis: contradiction
then ex F being Filter of BL st
( F = x & F is being_ultrafilter & Bottom BL in F ) by Th20;
hence contradiction by Th35; :: thesis: verum

end;

deffunc H₁( Subset of (ultraset BL), Subset of (ultraset BL)) -> Element of bool (ultraset BL) = $1 /\ $2;
consider G being BinOp of (bool (ultraset BL)) such that
A17: for x, y being Subset of (ultraset BL) holds G . (x,y) = H₁(x,y) from BINOP_1:sch 4();
A18: G is commutative

proof

let x, y be Subset of (ultraset BL); :: according to BINOP_1:def 13 :: thesis: G . (x,y) = G . (y,x)
G . (x,y) = y /\ x by A17
.= G . (y,x) by A17 ;
hence G . (x,y) = G . (y,x) ; :: thesis: verum

end;

A19: G is associative

proof

let x, y, z be Subset of (ultraset BL); :: according to BINOP_1:def 14 :: thesis: G . (x,(G . (y,z))) = G . ((G . (x,y)),z)
G . (x,(G . (y,z))) = G . (x,(y /\ z)) by A17
.= x /\ (y /\ z) by A17
.= (x /\ y) /\ z by XBOOLE_1:16
.= G . ((x /\ y),z) by A17
.= G . ((G . (x,y)),z) by A17 ;
hence G . (x,(G . (y,z))) = G . ((G . (x,y)),z) ; :: thesis: verum

end;

A20: G is idempotent

proof

let x be Subset of (ultraset BL); :: according to BINOP_1:def 15 :: thesis: G . (x,x) = x
G . (x,x) = x /\ x by A17
.= x ;
hence G . (x,x) = x ; :: thesis: verum

end;

A21: for x, y being Element of BL holds (UFilter BL) . ( the L_meet of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))

proof

let x, y be Element of BL; :: thesis: (UFilter BL) . ( the L_meet of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
thus (UFilter BL) . ( the L_meet of BL . (x,y)) = (UFilter BL) . (x "/\" y)
.= ((UFilter BL) . x) /\ ((UFilter BL) . y) by Th23
.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A17 ; :: thesis: verum

end;

reconsider DD = D as Element of Fin (bool (ultraset BL)) ;
id BL = id the carrier of BL ;
then A22: (UFilter BL) . (FinMeet B) = (UFilter BL) . (FinMeet (B,(id the carrier of BL))) by LATTICE4:def 13
.= (UFilter BL) . ( the L_meet of BL $$ (B,(id the carrier of BL))) by LATTICE2:def 4
.= G $$ (B,((UFilter BL) * (id the carrier of BL))) by A18, A19, A20, A21, SETWISEO:39
.= G $$ (B,(UFilter BL)) by FUNCT_2:23
.= G $$ (B,((id (bool (ultraset BL))) * (UFilter BL))) by FUNCT_2:23
.= G $$ (DD,(id (bool (ultraset BL)))) by A18, A19, A20, SETWISEO:38 ;
defpred S₁[ Element of Fin (bool (ultraset BL))] means for D being non empty Subset-Family of (ultraset BL) st D = $1 holds
G $$ ($1,(id (bool (ultraset BL)))) = meet D;
A23: S₁[ {}. (bool (ultraset BL))] ;
A24: for DD being Element of Fin (bool (ultraset BL))
for b being Subset of (ultraset BL) st S₁[DD] holds
S₁[DD \/ {.b.}]

proof

let DD be Element of Fin (bool (ultraset BL)); :: thesis: for b being Subset of (ultraset BL) st S₁[DD] holds
S₁[DD \/ {.b.}]
let b be Subset of (ultraset BL); :: thesis: ( S₁[DD] implies S₁[DD \/ {.b.}] )
assume A25: for D being non empty Subset-Family of (ultraset BL) st D = DD holds
G $$ (DD,(id (bool (ultraset BL)))) = meet D ; :: thesis: S₁[DD \/ {.b.}]
let D be non empty Subset-Family of (ultraset BL); :: thesis: ( D = DD \/ {.b.} implies G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D )
assume A26: D = DD \/ {b} ; :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D

now

per cases ( DD is empty or not DD is empty ) ;

suppose A27: DD is empty ; :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D

hence G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = (id (bool (ultraset BL))) . b by A18, A19, SETWISEO:26
.= b by FUNCT_1:35
.= meet D by A26, A27, SETFAM_1:11 ;
:: thesis: verum

end;

suppose A28: not DD is empty ; :: thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D

DD c= D by A26, XBOOLE_1:7;
then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by A28, XBOOLE_1:1;
reconsider D1 = D1 as non empty Subset-Family of (ultraset BL) ;
thus G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = G . ((G $$ (DD,(id (bool (ultraset BL))))),((id (bool (ultraset BL))) . b)) by A18, A19, A20, A28, SETWISEO:29
.= G . ((G $$ (DD,(id (bool (ultraset BL))))),b) by FUNCT_1:35
.= (G $$ (DD,(id (bool (ultraset BL))))) /\ b by A17
.= (meet D1) /\ b by A25
.= (meet D1) /\ (meet {b}) by SETFAM_1:11
.= meet D by A26, SETFAM_1:10 ; :: thesis: verum

end;

end;

end;

hence G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D ; :: thesis: verum

end;

for DD being Element of Fin (bool (ultraset BL)) holds S₁[DD] from SETWISEO:sch 4(A23, A24);
then meet D = {} (ultraset BL) by A12, A15, A22;
then A29: union (COMPLEMENT D) = ([#] (ultraset BL)) \ {} by SETFAM_1:48
.= ultraset BL ;
A30: COMPLEMENT D c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT D or x in X )
assume A31: x in COMPLEMENT D ; :: thesis: x in X
then reconsider c = x as Subset of (ultraset BL) ;
c ` in D by A31, SETFAM_1:def 8;
then consider a being set such that
A32: a in dom (UFilter BL) and
A33: a in B and
A34: c ` = (UFilter BL) . a by FUNCT_1:def 12;
reconsider a = a as Element of BL by A32;
a in CY by A11, A33;
then (a `) ` in CY by LATTICES:49;
then consider b being Element of BL such that
A35: b ` = (a `) ` and
A36: (UFilter BL) . b in X ;
x = ((UFilter BL) . a) ` by A34
.= (UFilter BL) . (a `) by Th28
.= (UFilter BL) . ((b `) `) by A35, LATTICES:49
.= (UFilter BL) . b by LATTICES:49 ;
hence x in X by A36; :: thesis: verum

end;

COMPLEMENT D is finite

proof

A37: D is finite ;
deffunc H₂( Subset of (ultraset BL)) -> Element of bool (ultraset BL) = $1 ` ;
A38: { H<sub>2</sub>(w) where w is Subset of (ultraset BL) : w in D } is finite from FRAENKEL:sch 21(A37);
{ (w `) where w is Subset of (ultraset BL) : w in D } = COMPLEMENT D

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: COMPLEMENT D c= { (w `) where w is Subset of (ultraset BL) : w in D }

let x be set ; :: thesis: ( x in { (w `) where w is Subset of (ultraset BL) : w in D } implies x in COMPLEMENT D )
assume x in { (w `) where w is Subset of (ultraset BL) : w in D } ; :: thesis: x in COMPLEMENT D
then consider w being Subset of (ultraset BL) such that
A39: w ` = x and
A40: w in D ;
(w `) ` in D by A40;
hence x in COMPLEMENT D by A39, SETFAM_1:def 8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT D or x in { (w `) where w is Subset of (ultraset BL) : w in D } )
assume A41: x in COMPLEMENT D ; :: thesis: x in { (w `) where w is Subset of (ultraset BL) : w in D }
then reconsider x9 = x as Subset of (ultraset BL) ;
A42: x9 ` in D by A41, SETFAM_1:def 8;
(x9 `) ` = x9 ;
hence x in { (w `) where w is Subset of (ultraset BL) : w in D } by A42; :: thesis: verum

end;

hence COMPLEMENT D is finite by A38; :: thesis: verum

end;

then COMPLEMENT D is Finite_Subset of X by A30, FINSUB_1:def 5;
hence contradiction by A3, A29; :: thesis: verum

end;

then <.CY.) <> the carrier of BL by Th34;
then consider F being Filter of BL such that
A43: <.CY.) c= F and
A44: F is being_ultrafilter by FILTER_0:22;
A45: CY c= <.CY.) by FILTER_0:def 5;
not F in union X

proof

assume F in union X ; :: thesis: contradiction
then consider Y being set such that
A46: F in Y and
A47: Y in X by TARSKI:def 4;
consider a being set such that
A48: a in dom (UFilter BL) and
A49: Y = (UFilter BL) . a by A2, A47, FUNCT_1:def 5;
reconsider a = a as Element of BL by A48;
a ` in CY by A47, A49;
then A50: a ` in <.CY.) by A45;
a in F by A46, A49, Th21;
hence contradiction by A43, A44, A50, FILTER_0:59; :: thesis: verum

end;

hence contradiction by A1, A44; :: thesis: verum