let T be TopAugmentation of R; :: thesis: T is trivial
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
hence T is trivial ; :: thesis: verum