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 T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) by YELLOW_9:def 4;
then A2: 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 S',the InternalRel of S' #) by YELLOW_9:def 4;
then UPS S,T = UPS S',T' by A1, Th25
.= SCMaps S',T' by Th24
.= ContMaps S',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