theorem Th15: :: WAYBEL29:15

for S being non empty up-complete Scott TopPoset holds Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)