let BL be non trivial B_Lattice; :: thesis:
A1: StoneR BL c= OpenClosedSet () by Lm2;
OpenClosedSet () c= StoneR BL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenClosedSet () or x in StoneR BL )
assume A2: x in OpenClosedSet () ; :: thesis: x in StoneR BL
then reconsider X = x as Subset of () ;
A3: the topology of () = { () where A is Subset-Family of (ultraset BL) : A c= StoneR BL } by Def8;
A4: ( X is open & X is closed ) by A2, Th1, Th2;
then A5: ( X ` is open & X ` is closed ) ;
X in the topology of () by ;
then consider A1 being Subset-Family of (ultraset BL) such that
A6: X = union A1 and
A7: A1 c= StoneR BL by A3;
X ` in the topology of () by ;
then consider A2 being Subset-Family of (ultraset BL) such that
A8: X ` = union A2 and
A9: A2 c= StoneR BL by A3;
A10: X is Subset of (ultraset BL) by Def8;
set AA = A1 \/ A2;
A11: ultraset BL = [#] () by Def8
.= X \/ (X `) by PRE_TOPC:2
.= union (A1 \/ A2) by ;
A12: A1 \/ A2 c= StoneR BL by ;
then consider Y being Element of Fin (A1 \/ A2) such that
A13: ultraset BL = union Y by ;
A14: Y c= A1 \/ A2 by FINSUB_1:def 5;
then A15: Y c= StoneR BL by A12;
set D = A1 /\ Y;
A16: Y = (A1 \/ A2) /\ Y by
.= (A1 /\ Y) \/ (A2 /\ Y) by XBOOLE_1:23 ;
now :: thesis: for y being set st y in A2 /\ Y holds
y misses X
let y be set ; :: thesis: ( y in A2 /\ Y implies y misses X )
assume y in A2 /\ Y ; :: thesis: y misses X
then y in A2 by XBOOLE_0:def 4;
then A17: y c= X ` by ;
X ` misses X by XBOOLE_1:79;
then (X `) /\ X = {} ;
then y /\ X = {} by ;
hence y misses X ; :: thesis: verum
end;
then A18: X c= union (A1 /\ Y) by ;
per cases ( A1 /\ Y = {} or A1 /\ Y <> {} ) ;
suppose A20: A1 /\ Y <> {} ; :: thesis: x in StoneR BL
A21: A1 /\ Y c= Y by XBOOLE_1:17;
reconsider D = A1 /\ Y as non empty Subset-Family of (ultraset BL) by A20;
reconsider D = D as non empty Subset-Family of (ultraset BL) ;
A22: union D c= (union A1) /\ () by ZFMISC_1:79;
(union A1) /\ () c= union A1 by XBOOLE_1:17;
then union D c= X by ;
then A23: X = union D by A18;
A24: D c= rng (UFilter BL) by ;
A25: rng (UFilter BL) = dom (id (StoneR BL)) ;
A26: dom (UFilter BL) = dom (UFilter BL) ;
UFilter BL = (id (StoneR BL)) * (UFilter BL) by RELAT_1:54;
then UFilter BL, id (StoneR BL) are_fiberwise_equipotent by ;
then card ((UFilter BL) " D) = card ((id (StoneR BL)) " D) by CLASSES1:78
.= card D by ;
then (UFilter BL) " D is finite ;
then reconsider B = (UFilter BL) " D as Element of Fin the carrier of BL by FINSUB_1:def 5;
A27: D = (UFilter BL) .: B by ;
then A28: not B is empty ;
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
A29: for x, y being Subset of (ultraset BL) holds G . (x,y) = H1(x,y) from A30: 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 A29
.= G . (y,x) by A29 ;
hence G . (x,y) = G . (y,x) ; :: thesis: verum
end;
A31: 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 A29
.= x \/ (y \/ z) by A29
.= (x \/ y) \/ z by XBOOLE_1:4
.= G . ((x \/ y),z) by A29
.= G . ((G . (x,y)),z) by A29 ;
hence G . (x,(G . (y,z))) = G . ((G . (x,y)),z) ; :: thesis: verum
end;
A32: 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 A29
.= x ;
hence G . (x,x) = x ; :: thesis: verum
end;
A33: for x, y being Element of BL holds (UFilter BL) . ( the L_join of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
proof
let x, y be Element of BL; :: thesis: (UFilter BL) . ( the L_join of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
thus (UFilter BL) . ( the L_join of BL . (x,y)) = (UFilter BL) . (x "\/" y)
.= ((UFilter BL) . x) \/ ((UFilter BL) . y) by Th21
.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A29 ; :: thesis: verum
end;
reconsider DD = D as Element of Fin (bool (ultraset BL)) by FINSUB_1:def 5;
id BL = id the carrier of BL ;
then A34: (UFilter BL) . () = (UFilter BL) . (FinJoin (B,(id the carrier of BL))) by LATTICE4:def 8
.= (UFilter BL) . ( the L_join of BL \$\$ (B,(id the carrier of BL))) by LATTICE2:def 3
.= 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)))) = union D;
A35: S1[ {}. (bool (ultraset BL))] ;
A36: 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 A37: for D being non empty Subset-Family of (ultraset BL) st D = DD holds
G \$\$ (DD,(id (bool (ultraset BL)))) = union 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)))) = union D )
assume A38: D = DD \/ {b} ; :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
now :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
per cases ( DD is empty or not DD is empty ) ;
suppose A39: DD is empty ; :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
hence G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = (id (bool (ultraset BL))) . b by
.= b
.= union D by ;
:: thesis: verum
end;
suppose A40: not DD is empty ; :: thesis: G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union 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 A29
.= (union D1) \/ b by A37
.= (union D1) \/ () by ZFMISC_1:25
.= union D by ; :: thesis: verum
end;
end;
end;
hence G \$\$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D ; :: thesis: verum
end;
for DD being Element of Fin (bool (ultraset BL)) holds S1[DD] from then (UFilter BL) . () = x by ;
hence x in StoneR BL by FUNCT_2:4; :: thesis: verum
end;
end;
end;
hence StoneR BL = OpenClosedSet () by A1; :: thesis: verum