let S, T be complete LATTICE; 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; verum