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