let S, T be complete LATTICE; :: thesis: UPS S,T is sups-inheriting SubRelStr of T |^ the carrier of S
consider S' being Scott TopAugmentation of S;
consider T' being Scott TopAugmentation of T;
A1: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) ) by YELLOW_9:def 4;
then A2: UPS S,T = UPS S',T' by Th25
.= SCMaps S',T' by Th24
.= ContMaps S',T' by WAYBEL24:38 ;
T' |^ the carrier of S = T |^ the carrier of S by A1, Th15;
hence UPS S,T is sups-inheriting SubRelStr of T |^ the carrier of S by A1, A2, WAYBEL24:35; :: thesis: verum