set S = Sigma (BoolePoset 1);
reconsider T = Omega Sierpinski_Space as strict Scott TopAugmentation of BoolePoset 1 by WAYBEL26:4;
A1: the topology of T = sigma (BoolePoset 1) by YELLOW_9:51
.= the topology of (Sigma (BoolePoset 1)) by YELLOW_9:51 ;
RelStr(# the carrier of T,the InternalRel of T #) = BoolePoset 1 by YELLOW_9:def 4
.= RelStr(# the carrier of (Sigma (BoolePoset 1)),the InternalRel of (Sigma (BoolePoset 1)) #) by YELLOW_9:def 4 ;
hence Omega Sierpinski_Space = Sigma (BoolePoset 1) by A1; :: thesis: verum