let S be non empty up-complete Scott TopPoset; :: thesis: Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
RelStr(# the carrier of TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #), the InternalRel of TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) #) = RelStr(# the carrier of S, the InternalRel of S #) ;
then reconsider T = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) as TopAugmentation of S by YELLOW_9:def 4;
T is Scott by Th14;
hence Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by Def1; :: thesis: verum