set S = the strict Scott TopAugmentation of BoolePoset 1;
A1: RelStr(# the carrier of the strict Scott TopAugmentation of BoolePoset 1, the InternalRel of the strict Scott TopAugmentation of BoolePoset 1 #) = BoolePoset 1 by YELLOW_9:def 4;
BoolePoset 1 = InclPoset (bool 1) by YELLOW_1:4;
then A2: the carrier of (BoolePoset 1) = {0,1} by YELLOW14:1, YELLOW_1:1;
( the carrier of Sierpinski_Space = {0,1} & the topology of the strict Scott TopAugmentation of BoolePoset 1 = the topology of Sierpinski_Space ) by WAYBEL18:12, WAYBEL18:def 9;
then Omega Sierpinski_Space = Omega the strict Scott TopAugmentation of BoolePoset 1 by A2, A1, WAYBEL25:13
.= the strict Scott TopAugmentation of BoolePoset 1 by WAYBEL25:15 ;
hence Omega Sierpinski_Space is TopAugmentation of BoolePoset 1 ; :: thesis: verum