let S, T be complete LATTICE; :: thesis: UPS S,T is sups-inheriting SubRelStr of T |^ the carrier of S
consider S9 being Scott TopAugmentation of S;
consider T9 being Scott TopAugmentation of T;
A1: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T9,the InternalRel of T9 #) by YELLOW_9:def 4;
then A2: T9 |^ the carrier of S = T |^ the carrier of S by Th15;
A3: 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 sups-inheriting SubRelStr of T |^ the carrier of S by A2, A3, WAYBEL24:35; :: thesis: verum