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