let S be TopAugmentation of L; :: thesis: S is up-complete
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
hence S is up-complete by WAYBEL_8:15; :: thesis: verum