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
object ;
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, 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
;
then A18:
X c= union (A1 /\ Y)
by A10, A13, A16, SETFAM_1:42;
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: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 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 BINOP_1:sch 4();
A30:
G is
commutative
A31:
G is
associative
proof
let x,
y,
z be
Subset of
(ultraset BL);
BINOP_1:def 3 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)
;
verum
end; A32:
G is
idempotent
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))
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) . (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 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));
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 A37:
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 A38:
D = DD \/ {b}
;
G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
now G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union Dper cases
( DD is empty or not DD is empty )
;
suppose A40:
not
DD is
empty
;
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
;
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(A35, A36);
then
(UFilter BL) . (FinJoin B) = x
by A23, A34;
hence
x in StoneR BL
by FUNCT_2:4;
verum end;
end;
hence
StoneR BL = OpenClosedSet (StoneSpace BL)
by A1; verum