set T = the Scott TopAugmentation of S;
A1: RelStr(# the carrier of (Omega the Scott TopAugmentation of S), the InternalRel of (Omega the Scott TopAugmentation of S) #) = RelStr(# the carrier of S, the InternalRel of S #) by Th16;
the topology of S = sigma S by WAYBEL14:23
.= the topology of the Scott TopAugmentation of S by YELLOW_9:51 ;
then TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of the Scott TopAugmentation of S, the topology of the Scott TopAugmentation of S #) by A1, Lm1;
then Omega S = Omega the Scott TopAugmentation of S by Th13;
hence Omega S is complete by A1, YELLOW_0:3; :: thesis: verum