let I be non empty set ; :: thesis:
set IB = I --> (BoolePoset {0});
set IS = I --> Sierpinski_Space;
A1: the carrier of (product (I --> (BoolePoset {0}))) = product (Carrier (I --> (BoolePoset {0}))) by YELLOW_1:def 4;
LattPOSet (BooleLatt {0}) = RelStr(# the carrier of (BooleLatt {0}),(LattRel (BooleLatt {0})) #) by LATTICE3:def 2;
then A2: the carrier of (BoolePoset {0}) = the carrier of (BooleLatt {0}) by YELLOW_1:def 2
.= bool {{}} by LATTICE3:def 1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A3: for i being object st i in dom (Carrier (I --> (BoolePoset {0}))) holds
(Carrier (I --> (BoolePoset {0}))) . i = (Carrier (I --> Sierpinski_Space)) . i

proof

let i be object ; :: thesis:
assume i in dom (Carrier (I --> (BoolePoset {0}))) ; :: thesis:
then A4: i in I ;
then consider R1 being 1-sorted such that
A5: R1 = (I --> (BoolePoset {0})) . i and
A6: (Carrier (I --> (BoolePoset {0}))) . i = the carrier of R1 by PRALG_1:def 15;
consider R2 being 1-sorted such that
A7: R2 = (I --> Sierpinski_Space) . i and
A8: (Carrier (I --> Sierpinski_Space)) . i = the carrier of R2 by A4, PRALG_1:def 15;
the carrier of R1 = {0,1} by A2, A4, A5, FUNCOP_1:7
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A4, A7, FUNCOP_1:7 ;
hence (Carrier (I --> (BoolePoset {0}))) . i = (Carrier (I --> Sierpinski_Space)) . i by A6, A8; :: thesis:

end;

reconsider P = { (product ((Carrier (I --> Sierpinski_Space)) +* (ii,{1}))) where ii is Element of I : verum } as prebasis of (product (I --> Sierpinski_Space)) by Th13;
let T be Scott TopAugmentation of product (I --> (BoolePoset {0})); :: thesis:
A9: dom (Carrier (I --> (BoolePoset {0}))) = I by PARTFUN1:def 2
.= dom (Carrier (I --> Sierpinski_Space)) by PARTFUN1:def 2 ;
reconsider T9 = T as complete Scott TopLattice ;
A10: RelStr(# the carrier of T, the InternalRel of T #) = product (I --> (BoolePoset {0})) by YELLOW_9:def 4;
then T9 is algebraic by WAYBEL_8:17;
then consider R being Basis of T9 such that
A11: R = { (uparrow yy) where yy is Element of T9 : yy in the carrier of (CompactSublatt T9) } by WAYBEL14:42;
A12: the carrier of T = product (Carrier (I --> (BoolePoset {0}))) by A10, YELLOW_1:def 4
.= product (Carrier (I --> Sierpinski_Space)) by A9, A3, FUNCT_1:2
.= the carrier of (product (I --> Sierpinski_Space)) by Def3 ;
then reconsider P9 = P as Subset-Family of T ;
consider f being Function of (BoolePoset I),(product (I --> (BoolePoset {0}))) such that
A13: f is isomorphic and
A14: for Y being Subset of I holds f . Y = chi (Y,I) by Th14;
A15: Carrier (I --> (BoolePoset {0})) = Carrier (I --> Sierpinski_Space) by A9, A3, FUNCT_1:2;
A16: FinMeetCl P c= R

proof

deffunc H₁( object ) -> set = product ((Carrier (I --> Sierpinski_Space)) +* ($1,{1}));
let X be object ; :: according to TARSKI:def 3 :: thesis:
consider F being Function such that
A17: dom F = I and
A18: for e being object st e in I holds
F . e = H₁(e) from FUNCT_1:sch 3();
assume A19: X in FinMeetCl P ; :: thesis:
then reconsider X9 = X as Subset of (product (I --> Sierpinski_Space)) ;
consider ZZ being Subset-Family of (product (I --> Sierpinski_Space)) such that
A20: ZZ c= P and
A21: ZZ is finite and
A22: X = Intersect ZZ by A19, CANTOR_1:def 3;
P c= rng F

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in P ; :: thesis:
then consider e being Element of I such that
A23: w = product ((Carrier (I --> Sierpinski_Space)) +* (e,{1})) ;
w = F . e by A18, A23;
hence w in rng F by A17, FUNCT_1:def 3; :: thesis:

end;

then ZZ c= rng F by A20;
then consider x9 being set such that
A24: x9 c= dom F and
A25: x9 is finite and
A26: F .: x9 = ZZ by A21, ORDERS_1:85;
reconsider x9 = x9 as Subset of I by A17, A24;
reconsider x = x9 as Element of (BoolePoset I) by WAYBEL_8:26;
reconsider y = f . x as Element of (product (I --> (BoolePoset {0}))) ;
set PP = { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } ;
A27: ZZ c= { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 }

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in ZZ ; :: thesis:
then consider e being object such that
A28: e in dom F and
A29: e in x9 and
A30: w = F . e by A26, FUNCT_1:def 6;
reconsider e = e as Element of I by A17, A28;
w = product ((Carrier (I --> Sierpinski_Space)) +* (e,{1})) by A18, A30;
hence w in { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } by A29; :: thesis:

end;

{ (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } c= ZZ

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } ; :: thesis:
then consider e being Element of I such that
A31: w = product ((Carrier (I --> Sierpinski_Space)) +* (e,{1})) and
A32: e in x9 ;
w = F . e by A18, A31;
hence w in ZZ by A17, A26, A32, FUNCT_1:def 6; :: thesis:

end;

then A33: ZZ = { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } by A27;
A34: uparrow y c= X9

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A35: z in uparrow y ; :: thesis:
then reconsider z9 = z as Element of (product (I --> (BoolePoset {0}))) ;
y <= z9 by A35, WAYBEL_0:18;
then consider h1, h2 being Function such that
A36: h1 = y and
A37: h2 = z9 and
A38: for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A1, YELLOW_1:def 4;
z in the carrier of (product (I --> (BoolePoset {0}))) by A35;
then z in product (Carrier (I --> (BoolePoset {0}))) by YELLOW_1:def 4;
then A39: ex gg being Function st
( z = gg & dom gg = dom (Carrier (I --> (BoolePoset {0}))) & ( for w being object st w in dom (Carrier (I --> (BoolePoset {0}))) holds
gg . w in (Carrier (I --> (BoolePoset {0}))) . w ) ) by CARD_3:def 5;
A40: h1 = chi (x,I) by A14, A36;
for Z being set st Z in ZZ holds
z in Z

proof

let Z be set ; :: thesis:
assume Z in ZZ ; :: thesis:
then consider j being Element of I such that
A41: Z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) and
A42: j in x by A33;
consider RS being RelStr , xj, yj being Element of RS such that
A43: RS = (I --> (BoolePoset {0})) . j and
A44: xj = h1 . j and
A45: yj = h2 . j and
A46: xj <= yj by A38;
A47: RS = BoolePoset {0} by A43;
A48: xj = 1 by A40, A42, A44, FUNCT_3:def 3;
A49: yj <> 0

proof

assume yj = 0 ; :: thesis:
then {0} c= 0 by A46, A48, A47, YELLOW_1:2, CARD_1:49;
hence contradiction ; :: thesis:

end;

reconsider b = yj as Element of (BoolePoset {0}) by A43;
A50: dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) = dom (Carrier (I --> Sierpinski_Space)) by FUNCT_7:30
.= I by PARTFUN1:def 2 ;
A51: b in the carrier of (BoolePoset {0}) ;
A52: for w being object st w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) holds
h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w

proof

let w be object ; :: thesis:
assume w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) ; :: thesis:
then A53: w in dom (Carrier (I --> Sierpinski_Space)) by A50, PARTFUN1:def 2;

per cases ;

suppose w = j ; :: thesis:

then ( ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = {1} & h2 . w = 1 ) by A2, A45, A51, A49, A53, FUNCT_7:31, TARSKI:def 2;
hence h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by TARSKI:def 1; :: thesis:

end;

suppose w <> j ; :: thesis:

then ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = (Carrier (I --> Sierpinski_Space)) . w by FUNCT_7:32;
hence h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by A15, A39, A37, A53; :: thesis:

end;

dom h2 = dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) by A39, A37, A50, PARTFUN1:def 2;
hence z in Z by A37, A41, A52, CARD_3:def 5; :: thesis:

end;

hence z in X9 by A10, A12, A22, A35, SETFAM_1:43; :: thesis:

end;

A54: X9 c= uparrow y

proof

set h1 = chi (x,I);
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A55: z in X9 ; :: thesis:
then reconsider z9 = z as Element of (product (I --> (BoolePoset {0}))) by A10, A12;
z in the carrier of (product (I --> (BoolePoset {0}))) by A10, A12, A55;
then z in product (Carrier (I --> (BoolePoset {0}))) by YELLOW_1:def 4;
then consider h2 being Function such that
A56: z = h2 and
dom h2 = dom (Carrier (I --> (BoolePoset {0}))) and
A57: for w being object st w in dom (Carrier (I --> (BoolePoset {0}))) holds
h2 . w in (Carrier (I --> (BoolePoset {0}))) . w by CARD_3:def 5;
A58: for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )

proof

let i be object ; :: thesis:
assume A59: i in I ; :: thesis:
then reconsider i9 = i as Element of I ;
ex RB being 1-sorted st
( RB = (I --> (BoolePoset {0})) . i & (Carrier (I --> (BoolePoset {0}))) . i = the carrier of RB ) by A59, PRALG_1:def 15;
then A60: (Carrier (I --> (BoolePoset {0}))) . i = {0,1} by A2, A59, FUNCOP_1:7;
take RS = BoolePoset {0}; :: thesis:
A61: i in dom (Carrier (I --> (BoolePoset {0}))) by A59, PARTFUN1:def 2;
then A62: h2 . i in (Carrier (I --> (BoolePoset {0}))) . i by A57;

per cases ;

suppose A63: i in x ; :: thesis:

end;

suppose A67: not i in x ; :: thesis:

thus ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) :: thesis:

proof

per cases by A60, A62, TARSKI:def 2;

suppose A68: h2 . i = 0 ; :: thesis:

reconsider xi = 0 , yi = 0 as Element of RS by A2, TARSKI:def 2;
take xi ; :: thesis:
take yi ; :: thesis:
thus RS = (I --> (BoolePoset {0})) . i by A59, FUNCOP_1:7; :: thesis:
thus xi = (chi (x,I)) . i by A59, A67, FUNCT_3:def 3; :: thesis:
thus yi = h2 . i by A68; :: thesis:
thus xi <= yi ; :: thesis:

end;

suppose A69: h2 . i = 1 ; :: thesis:

reconsider xi = 0 , yi = 1 as Element of RS by A2, TARSKI:def 2;
take xi ; :: thesis:
take yi ; :: thesis:
thus RS = (I --> (BoolePoset {0})) . i by A59, FUNCOP_1:7; :: thesis:
thus xi = (chi (x,I)) . i by A59, A67, FUNCT_3:def 3; :: thesis:
thus yi = h2 . i by A69; :: thesis:
xi c= yi ;
hence xi <= yi by YELLOW_1:2; :: thesis:

end;

chi (x,I) = y by A14;
then y <= z9 by A1, A56, A58, YELLOW_1:def 4;
hence z in uparrow y by WAYBEL_0:18; :: thesis:

end;

reconsider Y = y as Element of T9 by A10;
x is compact by A25, WAYBEL_8:28;
then y is compact by A13, WAYBEL13:28;
then Y is compact by A10, WAYBEL_8:9;
then A70: Y in the carrier of (CompactSublatt T9) by WAYBEL_8:def 1;
uparrow Y = uparrow {Y} by WAYBEL_0:def 18
.= uparrow {y} by A10, WAYBEL_0:13
.= uparrow y by WAYBEL_0:def 18 ;
then X = uparrow Y by A54, A34, XBOOLE_0:def 10;
hence X in R by A11, A70; :: thesis:

end;

A71: rng f = the carrier of (product (I --> (BoolePoset {0}))) by A13, WAYBEL_0:66;
R c= FinMeetCl P

proof

deffunc H₁( Element of I) -> set = product ((Carrier (I --> Sierpinski_Space)) +* ($1,{1}));
let X be object ; :: according to TARSKI:def 3 :: thesis:
assume A72: X in R ; :: thesis:
then consider Y being Element of T9 such that
A73: X = uparrow Y and
A74: Y in the carrier of (CompactSublatt T9) by A11;
reconsider X9 = X as Subset of (product (I --> Sierpinski_Space)) by A12, A72;
reconsider y = Y as Element of (product (I --> (BoolePoset {0}))) by A10;
consider x being object such that
A75: x in dom f and
A76: y = f . x by A71, FUNCT_1:def 3;
reconsider x = x as Element of (BoolePoset I) by A75;
Y is compact by A74, WAYBEL_8:def 1;
then y is compact by A10, WAYBEL_8:9;
then x is compact by A13, A76, WAYBEL13:28;
then A77: x is finite by WAYBEL_8:28;
A78: { H₁(jj) where jj is Element of I : jj in x } is finite from FRAENKEL:sch 21(A77);
set ZZ = { (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x } ;
reconsider x9 = x as Subset of I by WAYBEL_8:26;
A79: { (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x } c= P

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x } ; :: thesis:
then ex j being Element of I st
( z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) & j in x9 ) ;
hence z in P ; :: thesis:

end;

then reconsider ZZ = { (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x } as Subset-Family of (product (I --> Sierpinski_Space)) by XBOOLE_1:1;
A80: uparrow Y = uparrow {Y} by WAYBEL_0:def 18
.= uparrow {y} by A10, WAYBEL_0:13
.= uparrow y by WAYBEL_0:def 18 ;
A81: Intersect ZZ c= X9

proof

set h1 = chi (x,I);
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A82: z in Intersect ZZ ; :: thesis:
then reconsider z9 = z as Element of (product (I --> (BoolePoset {0}))) by A10, A12;
z in the carrier of (product (I --> (BoolePoset {0}))) by A10, A12, A82;
then z in product (Carrier (I --> (BoolePoset {0}))) by YELLOW_1:def 4;
then consider h2 being Function such that
A83: z = h2 and
dom h2 = dom (Carrier (I --> (BoolePoset {0}))) and
A84: for w being object st w in dom (Carrier (I --> (BoolePoset {0}))) holds
h2 . w in (Carrier (I --> (BoolePoset {0}))) . w by CARD_3:def 5;
A85: for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )

proof

let i be object ; :: thesis:
assume A86: i in I ; :: thesis:
then reconsider i9 = i as Element of I ;
ex RB being 1-sorted st
( RB = (I --> (BoolePoset {0})) . i & (Carrier (I --> (BoolePoset {0}))) . i = the carrier of RB ) by A86, PRALG_1:def 15;
then A87: (Carrier (I --> (BoolePoset {0}))) . i = {0,1} by A2, A86, FUNCOP_1:7;
take RS = BoolePoset {0}; :: thesis:
A88: i in dom (Carrier (I --> (BoolePoset {0}))) by A86, PARTFUN1:def 2;
then A89: h2 . i in (Carrier (I --> (BoolePoset {0}))) . i by A84;

per cases ;

suppose A90: i in x ; :: thesis:

end;

suppose A94: not i in x ; :: thesis:

thus ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) :: thesis:

proof

per cases by A87, A89, TARSKI:def 2;

suppose A95: h2 . i = 0 ; :: thesis:

reconsider xi = 0 , yi = 0 as Element of RS by A2, TARSKI:def 2;
take xi ; :: thesis:
take yi ; :: thesis:
thus RS = (I --> (BoolePoset {0})) . i by A86, FUNCOP_1:7; :: thesis:
thus xi = (chi (x,I)) . i by A86, A94, FUNCT_3:def 3; :: thesis:
thus yi = h2 . i by A95; :: thesis:
thus xi <= yi ; :: thesis:

end;

suppose A96: h2 . i = 1 ; :: thesis:

reconsider xi = 0 , yi = 1 as Element of RS by A2, TARSKI:def 2;
take xi ; :: thesis:
take yi ; :: thesis:
thus RS = (I --> (BoolePoset {0})) . i by A86, FUNCOP_1:7; :: thesis:
thus xi = (chi (x,I)) . i by A86, A94, FUNCT_3:def 3; :: thesis:
thus yi = h2 . i by A96; :: thesis:
xi c= yi ;
hence xi <= yi by YELLOW_1:2; :: thesis:

end;

chi (x,I) = f . x9 by A14
.= y by A76 ;
then y <= z9 by A1, A83, A85, YELLOW_1:def 4;
hence z in X9 by A73, A80, WAYBEL_0:18; :: thesis:

end;

X9 c= Intersect ZZ

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A97: z in X9 ; :: thesis:
then reconsider z9 = z as Element of (product (I --> (BoolePoset {0}))) by A10, A12;
y <= z9 by A73, A80, A97, WAYBEL_0:18;
then consider h1, h2 being Function such that
A98: h1 = y and
A99: h2 = z9 and
A100: for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A1, YELLOW_1:def 4;
z in the carrier of (product (I --> (BoolePoset {0}))) by A10, A12, A97;
then z in product (Carrier (I --> (BoolePoset {0}))) by YELLOW_1:def 4;
then A101: ex gg being Function st
( z = gg & dom gg = dom (Carrier (I --> (BoolePoset {0}))) & ( for w being object st w in dom (Carrier (I --> (BoolePoset {0}))) holds
gg . w in (Carrier (I --> (BoolePoset {0}))) . w ) ) by CARD_3:def 5;
A102: h1 = f . x9 by A76, A98
.= chi (x,I) by A14 ;
for Z being set st Z in ZZ holds
z in Z

proof

let Z be set ; :: thesis:
assume Z in ZZ ; :: thesis:
then consider j being Element of I such that
A103: Z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) and
A104: j in x ;
consider RS being RelStr , xj, yj being Element of RS such that
A105: RS = (I --> (BoolePoset {0})) . j and
A106: xj = h1 . j and
A107: yj = h2 . j and
A108: xj <= yj by A100;
reconsider a = xj, b = yj as Element of (BoolePoset {0}) by A105;
A109: a <= b by A105, A108;
A110: xj = 1 by A102, A104, A106, FUNCT_3:def 3;
A111: yj <> 0

proof

assume yj = 0 ; :: thesis:
then {0} c= 0 by A110, A109, YELLOW_1:2, CARD_1:49;
hence contradiction ; :: thesis:

end;

A112: dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) = dom (Carrier (I --> Sierpinski_Space)) by FUNCT_7:30
.= I by PARTFUN1:def 2 ;
A113: b in the carrier of (BoolePoset {0}) ;
A114: for w being object st w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) holds
h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w

proof

let w be object ; :: thesis:
assume w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) ; :: thesis:
then A115: w in dom (Carrier (I --> Sierpinski_Space)) by A112, PARTFUN1:def 2;

per cases ;

suppose w = j ; :: thesis:

then ( ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w = {1} & h2 . w = 1 ) by A2, A107, A113, A111, A115, FUNCT_7:31, TARSKI:def 2;
hence h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w by TARSKI:def 1; :: thesis:

end;

suppose w <> j ; :: thesis:

end;

dom h2 = dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) by A101, A99, A112, PARTFUN1:def 2;
hence z in Z by A99, A103, A114, CARD_3:def 5; :: thesis:

end;

hence z in Intersect ZZ by A97, SETFAM_1:43; :: thesis:

end;

then X9 = Intersect ZZ by A81;
hence X in FinMeetCl P by A79, A78, CANTOR_1:def 3; :: thesis:

end;

then R = FinMeetCl P by A16;
then P9 is prebasis of T by A12, YELLOW_9:23;
hence the topology of T = the topology of (product (I --> Sierpinski_Space)) by A12, YELLOW_9:26; :: thesis: