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 correct )
thus ( T is strict & T is Scott & T is correct ) by Th11, YELLOW_9:48; :: thesis: verum