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 Def4;
take T ; :: thesis: ( T is Scott & T is strict & T is correct )
thus ( T is Scott & T is strict & T is correct ) by Th48, Th49; :: thesis: verum