let BL be non trivial B_Lattice; :: thesis: StoneR BL = OpenClosedSet (StoneSpace BL)

A1: StoneR BL c= OpenClosedSet (StoneSpace BL) by Lm2;

OpenClosedSet (StoneSpace BL) c= StoneR BL

A1: StoneR BL c= OpenClosedSet (StoneSpace BL) by Lm2;

OpenClosedSet (StoneSpace BL) c= StoneR BL

proof

hence
StoneR BL = OpenClosedSet (StoneSpace BL)
by A1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenClosedSet (StoneSpace BL) or x in StoneR BL )

assume A2: x in OpenClosedSet (StoneSpace BL) ; :: thesis: x in StoneR BL

then reconsider X = x as Subset of (StoneSpace BL) ;

A3: the topology of (StoneSpace BL) = { (union A) 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 (StoneSpace BL) by A4, PRE_TOPC:def 2;

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 (StoneSpace BL) by A5, PRE_TOPC:def 2;

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 = [#] (StoneSpace BL) by Def8

.= X \/ (X `) by PRE_TOPC:2

.= union (A1 \/ A2) by A6, A8, ZFMISC_1:78 ;

A12: A1 \/ A2 c= StoneR BL by A7, A9, XBOOLE_1:8;

then consider Y being Element of Fin (A1 \/ A2) such that

A13: ultraset BL = union Y by A11, Th32;

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 A14, XBOOLE_1:28

.= (A1 /\ Y) \/ (A2 /\ Y) by XBOOLE_1:23 ;

end;assume A2: x in OpenClosedSet (StoneSpace BL) ; :: thesis: x in StoneR BL

then reconsider X = x as Subset of (StoneSpace BL) ;

A3: the topology of (StoneSpace BL) = { (union A) 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 (StoneSpace BL) by A4, PRE_TOPC:def 2;

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 (StoneSpace BL) by A5, PRE_TOPC:def 2;

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 = [#] (StoneSpace BL) by Def8

.= X \/ (X `) by PRE_TOPC:2

.= union (A1 \/ A2) by A6, A8, ZFMISC_1:78 ;

A12: A1 \/ A2 c= StoneR BL by A7, A9, XBOOLE_1:8;

then consider Y being Element of Fin (A1 \/ A2) such that

A13: ultraset BL = union Y by A11, Th32;

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 A14, XBOOLE_1:28

.= (A1 /\ Y) \/ (A2 /\ Y) by XBOOLE_1:23 ;

now :: thesis: for y being set st y in A2 /\ Y holds

y misses X

then A18:
X c= union (A1 /\ Y)
by A10, A13, A16, SETFAM_1:42;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 A8, ZFMISC_1:74;

X ` misses X by XBOOLE_1:79;

then (X `) /\ X = {} ;

then y /\ X = {} by A17, XBOOLE_1:3, XBOOLE_1:26;

hence y misses X ; :: thesis: verum

end;assume y in A2 /\ Y ; :: thesis: y misses X

then y in A2 by XBOOLE_0:def 4;

then A17: y c= X ` by A8, ZFMISC_1:74;

X ` misses X by XBOOLE_1:79;

then (X `) /\ X = {} ;

then y /\ X = {} by A17, XBOOLE_1:3, XBOOLE_1:26;

hence y misses X ; :: thesis: verum

per cases
( A1 /\ Y = {} or A1 /\ Y <> {} )
;

end;

suppose
A1 /\ Y = {}
; :: thesis: x in StoneR BL

then A19:
X = {}
by A18, ZFMISC_1:2;

{} = (UFilter BL) . (Bottom BL) by Th30;

hence x in StoneR BL by A19, FUNCT_2:4; :: thesis: verum

end;{} = (UFilter BL) . (Bottom BL) by Th30;

hence x in StoneR BL by A19, FUNCT_2:4; :: thesis: verum

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) /\ (union Y) by ZFMISC_1:79;

(union A1) /\ (union Y) c= union A1 by XBOOLE_1:17;

then union D c= X by A6, A22;

then A23: X = union D by A18;

A24: D c= rng (UFilter BL) by A15, A21;

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 A25, A26, CLASSES1:77;

then card ((UFilter BL) " D) = card ((id (StoneR BL)) " D) by CLASSES1:78

.= card D by A24, FUNCT_2:94 ;

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 A15, A21, FUNCT_1:77, XBOOLE_1:1;

then A28: not B is empty ;

deffunc H_{1}( 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) = H_{1}(x,y)
from BINOP_1:sch 4();

A30: G is commutative

id BL = id the carrier of BL ;

then A34: (UFilter BL) . (FinJoin B) = (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 A28, A30, A31, A32, A33, 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 A27, A28, A30, A31, A32, SETWISEO:29 ;

defpred S_{1}[ 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: S_{1}[ {}. (bool (ultraset BL))]
;

A36: for DD being Element of Fin (bool (ultraset BL))

for b being Subset of (ultraset BL) st S_{1}[DD] holds

S_{1}[DD \/ {.b.}]
_{1}[DD]
from SETWISEO:sch 4(A35, A36);

then (UFilter BL) . (FinJoin B) = x by A23, A34;

hence x in StoneR BL by FUNCT_2:4; :: thesis: verum

end;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) /\ (union Y) by ZFMISC_1:79;

(union A1) /\ (union Y) c= union A1 by XBOOLE_1:17;

then union D c= X by A6, A22;

then A23: X = union D by A18;

A24: D c= rng (UFilter BL) by A15, A21;

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 A25, A26, CLASSES1:77;

then card ((UFilter BL) " D) = card ((id (StoneR BL)) " D) by CLASSES1:78

.= card D by A24, FUNCT_2:94 ;

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 A15, A21, FUNCT_1:77, XBOOLE_1:1;

then A28: not B is empty ;

deffunc H

consider G being BinOp of (bool (ultraset BL)) such that

A29: for x, y being Subset of (ultraset BL) holds G . (x,y) = H

A30: G is commutative

proof

A31:
G is associative
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;G . (x,y) = y \/ x by A29

.= G . (y,x) by A29 ;

hence G . (x,y) = G . (y,x) ; :: thesis: verum

proof

A32:
G is idempotent
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;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

proof

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))
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;G . (x,x) = x \/ x by A29

.= x ;

hence G . (x,x) = x ; :: thesis: verum

proof

reconsider DD = D as Element of Fin (bool (ultraset BL)) by FINSUB_1:def 5;
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;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

id BL = id the carrier of BL ;

then A34: (UFilter BL) . (FinJoin B) = (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 A28, A30, A31, A32, A33, 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 A27, A28, A30, A31, A32, SETWISEO:29 ;

defpred S

G $$ ($1,(id (bool (ultraset BL)))) = union D;

A35: S

A36: for DD being Element of Fin (bool (ultraset BL))

for b being Subset of (ultraset BL) st S

S

proof

for DD being Element of Fin (bool (ultraset BL)) holds S
let DD be Element of Fin (bool (ultraset BL)); :: thesis: for b being Subset of (ultraset BL) st S_{1}[DD] holds

S_{1}[DD \/ {.b.}]

let b be Subset of (ultraset BL); :: thesis: ( S_{1}[DD] implies S_{1}[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: S_{1}[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

end;S

let b be Subset of (ultraset BL); :: thesis: ( S

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: S

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 Dend;

hence
G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
; :: thesis: verumper cases
( DD is empty or not DD is empty )
;

end;

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 A30, A31, SETWISEO:17

.= b

.= union D by A38, A39, ZFMISC_1:25 ;

:: thesis: verum

end;.= b

.= union D by A38, A39, ZFMISC_1:25 ;

:: thesis: verum

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

DD c= D
by A38, XBOOLE_1:7;

then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by A40, 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 A30, A31, A32, A40, SETWISEO:20

.= G . ((G $$ (DD,(id (bool (ultraset BL))))),b)

.= (G $$ (DD,(id (bool (ultraset BL))))) \/ b by A29

.= (union D1) \/ b by A37

.= (union D1) \/ (union {b}) by ZFMISC_1:25

.= union D by A38, ZFMISC_1:78 ; :: thesis: verum

end;then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by A40, 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 A30, A31, A32, A40, SETWISEO:20

.= G . ((G $$ (DD,(id (bool (ultraset BL))))),b)

.= (G $$ (DD,(id (bool (ultraset BL))))) \/ b by A29

.= (union D1) \/ b by A37

.= (union D1) \/ (union {b}) by ZFMISC_1:25

.= union D by A38, ZFMISC_1:78 ; :: thesis: verum

then (UFilter BL) . (FinJoin B) = x by A23, A34;

hence x in StoneR BL by FUNCT_2:4; :: thesis: verum