set T9 = the Scott TopAugmentation of T;
set S9 = the Scott TopAugmentation of S;
reconsider S9 = the Scott TopAugmentation of S, T9 = the Scott TopAugmentation of T 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