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