set S = the correct lower TopAugmentation of R;
A1: RelStr(# the carrier of the correct lower TopAugmentation of R, the InternalRel of the correct lower TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
then reconsider X = the topology of the correct lower TopAugmentation of R 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