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

A4: now :: thesis: for x being object st x in the topology of Sierpinski_Space holds
x in the topology of T

let x be object ; :: 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 {{},{{0}},{0,{0}}} by Def9, CARD_1:49;

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

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

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

end;

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

then reconsider x9 = x as Subset of T by A3, ZFMISC_1:7, CARD_1:49;
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 = {0} 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 5;
then j <= z by A2, A9, A11, ORDERS_2:def 5;
then {0} c= {} 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, CARD_1:49; :: 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:36;
then A14: 1 in D by TARSKI:def 1, TARSKI:def 2;
1 in x9 by A6, TARSKI:def 1, CARD_1:49;
hence D meets x9 by A14, XBOOLE_0:3; :: thesis: verum

end;

then x9 is inaccessible by WAYBEL11:def 1;
then x9 is open by A12, WAYBEL11:def 4;
hence x in the topology of T ; :: 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 :: thesis: for y being object st y in the topology of T holds
y in the topology of Sierpinski_Space

set a = 0 ;
set b = {0};
let y be object ; :: thesis: ( y in the topology of T implies y in the topology of Sierpinski_Space )
A15: not {0} in {z} ;
( 0 c= {0} & 0 in {z} ) by TARSKI:def 1;
then not {z} is upper by A15, WAYBEL_7:7;
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:36;
then y in {{},{1},{0,1}} by A17, A16, ENUMSET1:def 1;
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