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

A4: 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 A5: x in {{} ,{1},{0 ,1}} by Def9;

per cases ( x = {} or x = {1} or x = {0 ,1} ) by A5, 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 A6: x = {1} ; :: thesis: b₁ in the topology of T

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

proof

let a, b be Element of T; :: thesis: ( a in x9 & a <= b implies b in x9 )
assume that
A7: a in x9 and
A8: a <= b ; :: thesis: b in x9
A9: a = 1 by A6, A7, TARSKI:def 1;
A10: b <> 0

proof

assume A11: b = 0 ; :: thesis: contradiction
[a,b] in the InternalRel of T by A8, ORDERS_2:def 9;
then j <= z by A2, A9, A11, ORDERS_2:def 9;
then 1 c= 0 by YELLOW_1:2;
hence contradiction ; :: thesis: verum

end;

( b = 0 or b = 1 ) by A3, TARSKI:def 2;
hence b in x9 by A6, A10, TARSKI:def 1; :: thesis: verum

end;

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

proof

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

proof

assume D = {0 } ; :: thesis: contradiction
then sup D = sup {z} by A2, YELLOW_0:17, YELLOW_0:26
.= 0 by YELLOW_0:39 ;
hence contradiction by A6, A13, TARSKI:def 1; :: thesis: verum

end;

then ( D = {1} or D = {0 ,1} ) by A3, ZFMISC_1:42;
then A14: 1 in D by TARSKI:def 1, TARSKI:def 2;
1 in x9 by A6, TARSKI:def 1;
hence D meets x9 by A14, XBOOLE_0:3; :: thesis: verum

end;

then x9 is inaccessible_by_directed_joins by WAYBEL11:def 1;
then x9 is open by A12, 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;

reconsider c = {z} as Subset of T by A2;

now

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

end;

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