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
#)