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