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