consider S being correct lower TopAugmentation of R;
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) by YELLOW_9:def 4;
then reconsider X = the topology of S as Subset-Family of R ;
take X ; :: thesis: for T being correct lower TopAugmentation of R holds X = the topology of T
let T be correct lower TopAugmentation of R; :: thesis: X = the topology of T
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) by YELLOW_9:def 4;
hence X = the topology of T by A1, Th2; :: thesis: verum