let T be TopAugmentation of R; :: thesis: T is complete
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) by Def4;
hence T is complete by YELLOW_0:3; :: thesis: verum