theorem :: WAYBEL32:16

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )