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 A1, Th27, ZFMISC_1:2;
A5: Y c= X by FINSUB_1:def 5;
then A6: Y c= StoneR BL by A2, XBOOLE_1:1;
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 A13, A14, XBOOLE_1:1;

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 H₁( 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) = H₁(x,y) from BINOP_1:sch 4();
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) . (FinMeet B) = (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 A17, A18, A19, A20, SETWISEO:30
.= 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 A17, A18, A19, SETWISEO:29 ;
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;
A22: S₁[ {}. (bool (ultraset BL))] ;
A23: 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 A24: 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 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 A17, A18, SETWISEO:17
.= b
.= meet D by A25, A26, SETFAM_1:10 ;
:: thesis: verum

end;

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

DD c= D by A25, XBOOLE_1:7;
then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by A27, 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 A17, A18, A19, A27, SETWISEO:20
.= G . ((G $$ (DD,(id (bool (ultraset BL))))),b)
.= (G $$ (DD,(id (bool (ultraset BL))))) /\ b by A16
.= (meet D1) /\ b by A24
.= (meet D1) /\ (meet {b}) by SETFAM_1:10
.= meet D by A25, SETFAM_1:9 ; :: 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(A22, A23);
then meet D = {} (ultraset BL) by A12, A15, A21;
then A28: union (COMPLEMENT D) = ([#] (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 A30, SETFAM_1:def 7;
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 A11, A32;
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 H₂( Subset of (ultraset BL)) -> Element of K19((ultraset BL)) = $1 ` ;
A37: { H<sub>2</sub>(w) where w is Subset of (ultraset BL) : w in D } is finite from FRAENKEL:sch 21(A36);
{ (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: x in COMPLEMENT D
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 A38, SETFAM_1:def 7; :: 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 A40, SETFAM_1:def 7;
(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 A29, FINSUB_1:def 5;
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 A2, A46, FUNCT_1:def 3;
reconsider a = a as Element of BL by A47;
a ` in CY by A46, A48;
then A49: a ` in <.CY.) by A44;
a in F by A45, A48, Th18;
hence contradiction by A42, A43, A49, FILTER_0:46; :: thesis: verum

end;

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