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
proof
let x be
set ;
:: 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, Th2, Th3;
then A5:
(
X ` is
open &
X ` is
closed )
by TOPS_1:29, TOPS_1:30;
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 &
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 A7:
(
X ` = union A2 &
A2 c= StoneR BL )
by A3;
A8:
X is
Subset of
(ultraset BL)
by Def8;
set AA =
A1 \/ A2;
A9:
ultraset BL =
[#] (StoneSpace BL)
by Def8
.=
X \/ (X ` )
by PRE_TOPC:18
.=
union (A1 \/ A2)
by A6, A7, ZFMISC_1:96
;
A10:
A1 \/ A2 c= StoneR BL
by A6, A7, XBOOLE_1:8;
then consider Y being
Finite_Subset of
(A1 \/ A2) such that A11:
ultraset BL = union Y
by A9, Th38;
A12:
Y c= A1 \/ A2
by FINSUB_1:def 5;
then A13:
Y c= StoneR BL
by A10, XBOOLE_1:1;
set D =
A1 /\ Y;
A14:
Y =
(A1 \/ A2) /\ Y
by A12, XBOOLE_1:28
.=
(A1 /\ Y) \/ (A2 /\ Y)
by XBOOLE_1:23
;
then A16:
X c= union (A1 /\ Y)
by A8, A11, A14, SETFAM_1:57;
per cases
( A1 /\ Y = {} or A1 /\ Y <> {} )
;
suppose A18:
A1 /\ Y <> {}
;
:: thesis: x in StoneR BLA19:
A1 /\ Y c= Y
by XBOOLE_1:17;
reconsider D =
A1 /\ Y as non
empty Subset-Family of
(ultraset BL) by A18;
reconsider D =
D as non
empty Subset-Family of
(ultraset BL) ;
union D c= X
then A21:
X = union D
by A16, XBOOLE_0:def 10;
A22:
D c= rng (UFilter BL)
by A13, A19, XBOOLE_1:1;
A23:
rng (UFilter BL) = dom (id (StoneR BL))
by FUNCT_2:def 1;
(
dom (UFilter BL) = dom (UFilter BL) &
UFilter BL is
one-to-one &
UFilter BL = (id (StoneR BL)) * (UFilter BL) )
by Th29, RELAT_1:80;
then
UFilter BL,
id (StoneR BL) are_fiberwise_equipotent
by A23, CLASSES1:85;
then card ((UFilter BL) " D) =
card ((id (StoneR BL)) " D)
by CLASSES1:86
.=
card D
by A22, FUNCT_2:171
;
then
card ((UFilter BL) " D) is
finite
;
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;
A24:
D = (UFilter BL) .: B
by A13, A19, FUNCT_1:147, XBOOLE_1:1;
then A25:
not
B is
empty
by RELAT_1:149;
A26:
( the
L_join of
BL is
commutative & the
L_join of
BL is
associative & the
L_join of
BL is
idempotent )
by LATTICE2:26, LATTICE2:27, LATTICE2:29;
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 A27:
for
x,
y being
Subset of
(ultraset BL) holds
G . x,
y = H1(
x,
y)
from BINOP_1:sch 4();
A28:
G is
commutative
A29:
G is
associative
proof
let x,
y,
z be
Subset of
(ultraset BL);
:: according to BINOP_1:def 14 :: thesis: G . x,(G . y,z) = G . (G . x,y),z
G . x,
(G . y,z) =
G . x,
(y \/ z)
by A27
.=
x \/ (y \/ z)
by A27
.=
(x \/ y) \/ z
by XBOOLE_1:4
.=
G . (x \/ y),
z
by A27
.=
G . (G . x,y),
z
by A27
;
hence
G . x,
(G . y,z) = G . (G . x,y),
z
;
:: thesis: verum
end; A30:
G is
idempotent
A31:
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 A32:
(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 A25, A26, A28, A29, A30, A31, 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 A24, A25, A28, A29, A30, 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;
A33:
S1[
{}. (bool (ultraset BL))]
;
A34:
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 A35:
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 A36:
D = DD \/ {b}
;
:: thesis: G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = union D
now per cases
( DD is empty or not DD is empty )
;
suppose A38:
not
DD is
empty
;
:: thesis: G $$ (DD \/ {.b.}),(id (bool (ultraset BL))) = union D
DD c= D
by A36, XBOOLE_1:7;
then reconsider D1 =
DD as non
empty Subset-Family of
(ultraset BL) by A38, 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 A28, A29, A30, A38, SETWISEO:29
.=
G . (G $$ DD,(id (bool (ultraset BL)))),
b
by FUNCT_1:35
.=
(G $$ DD,(id (bool (ultraset BL)))) \/ b
by A27
.=
(union D1) \/ b
by A35
.=
(union D1) \/ (union {b})
by ZFMISC_1:31
.=
union D
by A36, ZFMISC_1:96
;
:: thesis: verum 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 SETWISEO:sch 4(A33, A34);
then
(UFilter BL) . (FinJoin B) = x
by A21, A32;
hence
x in StoneR BL
by FUNCT_2:6;
:: thesis: verum end;
end;
hence
StoneR BL = OpenClosedSet (StoneSpace BL)
by A1, XBOOLE_0:def 10; :: thesis: verum