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 Th18;
hence Sigma S = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #) by Def1; :: thesis: verum