theorem Th7: :: WAYBEL11:7

for T being non empty reflexive transitive up-complete Scott TopRelStr
for S being Subset of T holds
( S is closed iff ( S is directly_closed & S is lower ) )