let S1, S2 be strict Scott TopAugmentation of L; :: thesis: S1 = S2
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def 4;
hence S1 = S2 by Th13; :: thesis: verum