set T = TopRelStr(# the carrier of R,the InternalRel of R,(sigma R) #);
RelStr(# the carrier of TopRelStr(# the carrier of R,the InternalRel of R,(sigma R) #),the InternalRel of TopRelStr(# the carrier of R,the InternalRel of R,(sigma R) #) #) = RelStr(# the carrier of R,the InternalRel of R #) ;
then reconsider T = TopRelStr(# the carrier of R,the InternalRel of R,(sigma R) #) as TopAugmentation of R by YELLOW_9:def 4;
take T ; :: thesis: ( T is strict & T is Scott & T is TopSpace-like )
thus ( T is strict & T is Scott & T is TopSpace-like ) by Th15, YELLOW_9:48; :: thesis: verum