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