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