set T = the strict Scott TopAugmentation of Omega S;
A1: TopStruct(# the carrier of the strict Scott TopAugmentation of Omega S, the topology of the strict Scott TopAugmentation of Omega S #) = TopStruct(# the carrier of S, the topology of S #) by WAYBEL25:37
.= TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) by WAYBEL25:def 2 ;
RelStr(# the carrier of the strict Scott TopAugmentation of Omega S, the InternalRel of the strict Scott TopAugmentation of Omega S #) = RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) by YELLOW_9:def 4;
hence Omega S is Scott by A1; :: thesis: verum