consider T' being Scott TopAugmentation of T;
consider S' being Scott TopAugmentation of S;
reconsider S' = S', T' = T' as complete Scott TopLattice ;
A1: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) by YELLOW_9:def 4;
RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) by YELLOW_9:def 4;
then UPS S,T = UPS S',T' by A1, Th25
.= SCMaps S',T' by Th24
.= ContMaps S',T' by WAYBEL24:38 ;
hence UPS S,T is complete ; :: thesis: verum