let BL be non trivial B_Lattice; StoneR BL = OpenClosedSet (StoneSpace BL)
A1:
StoneR BL c= OpenClosedSet (StoneSpace BL)
by Lm2;
OpenClosedSet (StoneSpace BL) c= StoneR BL
proof
let x be
set ;
TARSKI:def 3 ( not x in OpenClosedSet (StoneSpace BL) or x in StoneR BL )
assume A2:
x in OpenClosedSet (StoneSpace BL)
;
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, Th2, Th3;
then A5:
(
X ` is
open &
X ` is
closed )
;
X in the
topology of
(StoneSpace BL)
by A4, PRE_TOPC:def 5;
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 5;
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:18
.=
union (A1 \/ A2)
by A6, A8, ZFMISC_1:96
;
A12:
A1 \/ A2 c= StoneR BL
by A7, A9, XBOOLE_1:8;
then consider Y being
Finite_Subset of
(A1 \/ A2) such that A13:
ultraset BL = union Y
by A11, Th38;
A14:
Y c= A1 \/ A2
by FINSUB_1:def 5;
then A15:
Y c= StoneR BL
by A12, XBOOLE_1:1;
set D =
A1 /\ Y;
A16:
Y =
(A1 \/ A2) /\ Y
by A14, XBOOLE_1:28
.=
(A1 /\ Y) \/ (A2 /\ Y)
by XBOOLE_1:23
;
then A18:
X c= union (A1 /\ Y)
by A10, A13, A16, SETFAM_1:57;
per cases
( A1 /\ Y = {} or A1 /\ Y <> {} )
;
suppose A20:
A1 /\ Y <> {}
;
x in StoneR BLA21:
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:97;
(union A1) /\ (union Y) c= union A1
by XBOOLE_1:17;
then
union D c= X
by A6, A22, XBOOLE_1:1;
then A23:
X = union D
by A18, XBOOLE_0:def 10;
A24:
D c= rng (UFilter BL)
by A15, A21, XBOOLE_1:1;
A25:
rng (UFilter BL) = dom (id (StoneR BL))
by FUNCT_2:def 1;
A26:
dom (UFilter BL) = dom (UFilter BL)
;
UFilter BL = (id (StoneR BL)) * (UFilter BL)
by RELAT_1:80;
then
UFilter BL,
id (StoneR BL) are_fiberwise_equipotent
by A25, A26, CLASSES1:85;
then card ((UFilter BL) " D) =
card ((id (StoneR BL)) " D)
by CLASSES1:86
.=
card D
by A24, FUNCT_2:171
;
then
(UFilter BL) " D is
finite
;
then reconsider B =
(UFilter BL) " D as
Finite_Subset of the
carrier of
BL by FINSUB_1:def 5;
A28:
D = (UFilter BL) .: B
by A15, A21, FUNCT_1:147, XBOOLE_1:1;
then A29:
not
B is
empty
by RELAT_1:149;
deffunc H1(
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 A33:
for
x,
y being
Subset of
(ultraset BL) holds
G . x,
y = H1(
x,
y)
from BINOP_1:sch 4();
A34:
G is
commutative
A35:
G is
associative
proof
let x,
y,
z be
Subset of
(ultraset BL);
BINOP_1:def 14 G . x,(G . y,z) = G . (G . x,y),z
G . x,
(G . y,z) =
G . x,
(y \/ z)
by A33
.=
x \/ (y \/ z)
by A33
.=
(x \/ y) \/ z
by XBOOLE_1:4
.=
G . (x \/ y),
z
by A33
.=
G . (G . x,y),
z
by A33
;
hence
G . x,
(G . y,z) = G . (G . x,y),
z
;
verum
end; A36:
G is
idempotent
A37:
for
x,
y being
Element of
BL holds
(UFilter BL) . (the L_join of BL . x,y) = G . ((UFilter BL) . x),
((UFilter BL) . y)
reconsider DD =
D as
Element of
Fin (bool (ultraset BL)) by FINSUB_1:def 5;
id BL = id the
carrier of
BL
;
then A38:
(UFilter BL) . (FinJoin B) =
(UFilter BL) . (FinJoin B,(id the carrier of BL))
by LATTICE4:def 12
.=
(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 A29, A34, A35, A36, A37, 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 A28, A29, A34, A35, A36, SETWISEO:38
;
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;
A39:
S1[
{}. (bool (ultraset BL))]
;
A40:
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));
for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]let b be
Subset of
(ultraset BL);
( S1[DD] implies S1[DD \/ {.b.}] )
assume A41:
for
D being non
empty Subset-Family of
(ultraset BL) st
D = DD holds
G $$ DD,
(id (bool (ultraset BL))) = union D
;
S1[DD \/ {.b.}]
let D be non
empty Subset-Family of
(ultraset BL);
( D = DD \/ {.b.} implies G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = union D )
assume A42:
D = DD \/ {b}
;
G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = union D
now per cases
( DD is empty or not DD is empty )
;
suppose A44:
not
DD is
empty
;
G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = union D
DD c= D
by A42, XBOOLE_1:7;
then reconsider D1 =
DD as non
empty Subset-Family of
(ultraset BL) by A44, 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 A34, A35, A36, A44, SETWISEO:29
.=
G . (G $$ DD,(id (bool (ultraset BL)))),
b
by FUNCT_1:35
.=
(G $$ DD,(id (bool (ultraset BL)))) \/ b
by A33
.=
(union D1) \/ b
by A41
.=
(union D1) \/ (union {b})
by ZFMISC_1:31
.=
union D
by A42, ZFMISC_1:96
;
verum end;
hence
G $$ (DD \/ {.b.}),
(id (bool (ultraset BL))) = union D
;
verum
end;
for
DD being
Element of
Fin (bool (ultraset BL)) holds
S1[
DD]
from SETWISEO:sch 4(A39, A40);
then
(UFilter BL) . (FinJoin B) = x
by A23, A38;
hence
x in StoneR BL
by FUNCT_2:6;
verum end;
end;
hence
StoneR BL = OpenClosedSet (StoneSpace BL)
by A1, XBOOLE_0:def 10; verum