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 Element of Fin 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 Element of Fin 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 Element of Fin X st ultraset BL = union Y
assume A3: for Y being Element of Fin X holds not ultraset BL = union Y ; :: thesis: contradiction
consider Y being Element of Fin X such that
A4: not Y is empty by ;
A5: Y c= X by FINSUB_1:def 5;
then A6: Y c= StoneR BL by ;
set x = the Element of Y;
A7: the Element of Y in X by A4, A5;
the Element of Y in StoneR BL by A4, A6;
then consider b being Element of BL such that
A8: the Element of Y = (UFilter BL) . b by Th23;
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 object ; :: 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 Element of Fin the carrier of BL st B c= CY holds
FinMeet B <> Bottom BL
proof
let B be non empty Element of Fin 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:16;
A14: dom (UFilter BL) = the carrier of BL by FUNCT_2:def 1;
(UFilter BL) .: B c= rng (UFilter BL) by RELAT_1:111;
then reconsider D = (UFilter BL) .: B as non empty Subset-Family of (ultraset BL) by ;
A15: now :: thesis: not {} (ultraset BL) <> (UFilter BL) . (Bottom BL)
set x = the Element of (UFilter BL) . (Bottom BL);
assume {} (ultraset BL) <> (UFilter BL) . (Bottom BL) ; :: thesis: contradiction
then ex F being Filter of BL st
( F = the Element of (UFilter BL) . (Bottom BL) & F is being_ultrafilter & Bottom BL in F ) by Th17;
hence contradiction by Th29; :: thesis: verum
end;
deffunc H1( Subset of (ultraset BL), Subset of (ultraset BL)) -> Element of K19((ultraset BL)) = \$1 /\ \$2;
consider G being BinOp of (bool (ultraset BL)) such that
A16: for x, y being Subset of (ultraset BL) holds G . (x,y) = H1(x,y) from A17: G is commutative
proof
let x, y be Subset of (ultraset BL); :: according to BINOP_1:def 2 :: thesis: G . (x,y) = G . (y,x)
G . (x,y) = y /\ x by A16
.= G . (y,x) by A16 ;
hence G . (x,y) = G . (y,x) ; :: thesis: verum
end;
A18: G is associative
proof
let x, y, z be Subset of (ultraset BL); :: according to BINOP_1:def 3 :: thesis: G . (x,(G . (y,z))) = G . ((G . (x,y)),z)
G . (x,(G . (y,z))) = G . (x,(y /\ z)) by A16
.= x /\ (y /\ z) by A16
.= (x /\ y) /\ z by XBOOLE_1:16
.= G . ((x /\ y),z) by A16
.= G . ((G . (x,y)),z) by A16 ;
hence G . (x,(G . (y,z))) = G . ((G . (x,y)),z) ; :: thesis: verum
end;
A19: G is idempotent
proof
let x be Subset of (ultraset BL); :: according to BINOP_1:def 4 :: thesis: G . (x,x) = x
G . (x,x) = x /\ x by A16
.= x ;
hence G . (x,x) = x ; :: thesis: verum
end;
A20: 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 Th20
.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A16 ; :: thesis: verum
end;
reconsider DD = D as Element of Fin (bool (ultraset BL)) ;
id BL = id the carrier of BL ;
then A21: (UFilter BL) . () = (UFilter BL) . (FinMeet (B,(id the carrier of BL))) by LATTICE4:def 9
.= (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
.= G \$\$ (B,(UFilter BL)) by FUNCT_2:17
.= G \$\$ (B,((id (bool (ultraset BL))) * (UFilter BL))) by FUNCT_2:17
.= G \$\$ (DD,(id (bool (ultraset BL)))) by ;
defpred S1[ 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;
A22: S1[ {}. (bool (ultraset BL))] ;
A23: for DD being Element of Fin (bool (ultraset BL))
for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]
proof
let DD be Element of Fin (bool (ultraset BL)); :: thesis: for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]

let b be Subset of (ultraset BL); :: thesis: ( S1[DD] implies S1[DD \/ {.b.}] )
assume A24: for D being non empty Subset-Family of (ultraset BL) st D = DD holds
G \$\$ (DD,(id (bool (ultraset BL)))) = meet D ; :: thesis: S1[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 A25: D = DD \/ {b} ; :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
now :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
per cases ( DD is empty or not DD is empty ) ;
suppose A26: 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
.= b
.= meet D by ;
:: thesis: verum
end;
suppose A27: not DD is empty ; :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
DD c= D by ;
then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by ;
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
.= G . ((G \$\$ (DD,(id (bool (ultraset BL))))),b)
.= (G \$\$ (DD,(id (bool (ultraset BL))))) /\ b by A16
.= (meet D1) /\ b by A24
.= (meet D1) /\ () by SETFAM_1:10
.= meet D by ; :: 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 S1[DD] from then meet D = {} (ultraset BL) by ;
then A28: union () = ([#] (ultraset BL)) \ {} by SETFAM_1:34
.= ultraset BL ;
A29: COMPLEMENT D c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT D or x in X )
assume A30: x in COMPLEMENT D ; :: thesis: x in X
then reconsider c = x as Subset of (ultraset BL) ;
c ` in D by ;
then consider a being object such that
A31: a in dom (UFilter BL) and
A32: a in B and
A33: c ` = (UFilter BL) . a by FUNCT_1:def 6;
reconsider a = a as Element of BL by A31;
a in CY by ;
then (a `) ` in CY ;
then consider b being Element of BL such that
A34: b ` = (a `) ` and
A35: (UFilter BL) . b in X ;
x = ((UFilter BL) . a) ` by A33
.= (UFilter BL) . (a `) by Th25
.= (UFilter BL) . ((b `) `) by A34
.= (UFilter BL) . b ;
hence x in X by A35; :: thesis: verum
end;
COMPLEMENT D is finite
proof
A36: D is finite ;
deffunc H2( Subset of (ultraset BL)) -> Element of K19((ultraset BL)) = \$1 ` ;
A37: { H2(w) where w is Subset of (ultraset BL) : w in D } is finite from { (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 object ; :: 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:
then consider w being Subset of (ultraset BL) such that
A38: w ` = x and
A39: w in D ;
(w `) ` in D by A39;
hence x in COMPLEMENT D by ; :: thesis: verum
end;
let x be object ; :: 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 A40: 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) ;
A41: x9 ` in D by ;
(x9 `) ` = x9 ;
hence x in { (w `) where w is Subset of (ultraset BL) : w in D } by A41; :: thesis: verum
end;
hence COMPLEMENT D is finite by A37; :: thesis: verum
end;
then COMPLEMENT D is Element of Fin X by ;
hence contradiction by A3, A28; :: thesis: verum
end;
then <.CY.) <> the carrier of BL by Th28;
then consider F being Filter of BL such that
A42: <.CY.) c= F and
A43: F is being_ultrafilter by FILTER_0:18;
A44: CY c= <.CY.) by FILTER_0:def 4;
not F in union X
proof
assume F in union X ; :: thesis: contradiction
then consider Y being set such that
A45: F in Y and
A46: Y in X by TARSKI:def 4;
consider a being object such that
A47: a in dom (UFilter BL) and
A48: Y = (UFilter BL) . a by ;
reconsider a = a as Element of BL by A47;
a ` in CY by ;
then A49: a ` in <.CY.) by A44;
a in F by ;
hence contradiction by A42, A43, A49, FILTER_0:46; :: thesis: verum
end;
hence contradiction by A1, A43; :: thesis: verum