let T be Scott TopAugmentation of BoolePoset 1; :: thesis: the topology of T = the topology of Sierpinski_Space
A1: RelStr(# the carrier of T,the InternalRel of T #) = BoolePoset 1 by YELLOW_9:def 4;
A2: LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def 2;
A3: the carrier of T = the carrier of (LattPOSet (BooleLatt 1)) by A1, YELLOW_1:def 2
.= bool 1 by A2, LATTICE3:def 1
.= {0 ,1} by CARD_1:87, ZFMISC_1:30 ;
then reconsider j = 1, z = 0 as Element of (BoolePoset 1) by A1, TARSKI:def 2;
reconsider c = {z} as Subset of T by A1;

A4: now

let y be set ; :: thesis: ( y in the topology of T implies y in the topology of Sierpinski_Space )
assume A5: y in the topology of T ; :: thesis: y in the topology of Sierpinski_Space
then reconsider x = y as Subset of T ;
A6: ( x = {} or x = {0 } or x = {1} or x = {0 ,1} ) by A3, ZFMISC_1:42;
set a = 0 ;
set b = 1;
A7: 0 c= 1 by XBOOLE_1:2;
A8: 0 in {z} by TARSKI:def 1;
not 1 in {z} by TARSKI:def 1;
then not {z} is upper by A7, A8, WAYBEL_7:11;
then not c is upper by A1, WAYBEL_0:25;
then not c is open by WAYBEL11:def 4;
then y in {{} ,{1},{0 ,1}} by A5, A6, ENUMSET1:def 1, PRE_TOPC:def 5;
hence y in the topology of Sierpinski_Space by Def9; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in the topology of Sierpinski_Space implies b₁ in the topology of T )
assume x in the topology of Sierpinski_Space ; :: thesis: b₁ in the topology of T
then A9: x in {{} ,{1},{0 ,1}} by Def9;

per cases ( x = {} or x = {1} or x = {0 ,1} ) by A9, ENUMSET1:def 1;

suppose x = {} ; :: thesis: b₁ in the topology of T

hence x in the topology of T by PRE_TOPC:5; :: thesis: verum

end;

suppose A10: x = {1} ; :: thesis: b₁ in the topology of T

then reconsider x' = x as Subset of T by A3, ZFMISC_1:12;
for a, b being Element of T st a in x' & a <= b holds
b in x'

proof

let a, b be Element of T; :: thesis: ( a in x' & a <= b implies b in x' )
assume that
A11: a in x' and
A12: a <= b ; :: thesis: b in x'
A13: a = 1 by A10, A11, TARSKI:def 1;
A14: ( b = 0 or b = 1 ) by A3, TARSKI:def 2;
b <> 0

proof

assume A15: b = 0 ; :: thesis: contradiction
[a,b] in the InternalRel of T by A12, ORDERS_2:def 9;
then j <= z by A1, A13, A15, ORDERS_2:def 9;
then A16: 1 c= 0 by YELLOW_1:2;
thus contradiction by A16; :: thesis: verum

end;

hence b in x' by A10, A14, TARSKI:def 1; :: thesis: verum

end;

then A17: x' is upper by WAYBEL_0:def 20;
for D being non empty directed Subset of T st sup D in x' holds
D meets x'

proof

let D be non empty directed Subset of T; :: thesis: ( sup D in x' implies D meets x' )
assume A18: sup D in x' ; :: thesis: D meets x'
D <> {0 }

proof

assume A19: D = {0 } ; :: thesis: contradiction
ex_sup_of D, BoolePoset 1 by YELLOW_0:17;
then sup D = sup {z} by A1, A19, YELLOW_0:26
.= 0 by YELLOW_0:39 ;
hence contradiction by A10, A18, TARSKI:def 1; :: thesis: verum

end;

then ( D = {1} or D = {0 ,1} ) by A3, ZFMISC_1:42;
then A20: 1 in D by TARSKI:def 1, TARSKI:def 2;
1 in x' by A10, TARSKI:def 1;
hence D meets x' by A20, XBOOLE_0:3; :: thesis: verum

end;

then x' is inaccessible_by_directed_joins by WAYBEL11:def 1;
then x' is open by A17, WAYBEL11:def 4;
hence x in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

suppose x = {0 ,1} ; :: thesis: b₁ in the topology of T

hence x in the topology of T by A3, PRE_TOPC:def 1; :: thesis: verum

end;

end;

end;

hence the topology of T = the topology of Sierpinski_Space by A4, TARSKI:2; :: thesis: verum