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