set S = Sigma (BoolePoset {0});

reconsider T = Omega Sierpinski_Space as strict Scott TopAugmentation of BoolePoset {0} by WAYBEL26:4;

A1: the topology of T = sigma (BoolePoset {0}) by YELLOW_9:51

.= the topology of (Sigma (BoolePoset {0})) by YELLOW_9:51 ;

RelStr(# the carrier of T, the InternalRel of T #) = BoolePoset {0} by YELLOW_9:def 4

.= RelStr(# the carrier of (Sigma (BoolePoset {0})), the InternalRel of (Sigma (BoolePoset {0})) #) by YELLOW_9:def 4 ;

hence Omega Sierpinski_Space = Sigma (BoolePoset {0}) by A1; :: thesis: verum

reconsider T = Omega Sierpinski_Space as strict Scott TopAugmentation of BoolePoset {0} by WAYBEL26:4;

A1: the topology of T = sigma (BoolePoset {0}) by YELLOW_9:51

.= the topology of (Sigma (BoolePoset {0})) by YELLOW_9:51 ;

RelStr(# the carrier of T, the InternalRel of T #) = BoolePoset {0} by YELLOW_9:def 4

.= RelStr(# the carrier of (Sigma (BoolePoset {0})), the InternalRel of (Sigma (BoolePoset {0})) #) by YELLOW_9:def 4 ;

hence Omega Sierpinski_Space = Sigma (BoolePoset {0}) by A1; :: thesis: verum