theorem Th8: :: WAYBEL11:8

for T being non empty reflexive transitive antisymmetric up-complete TopRelStr
for x being Element of T holds downarrow x is directly_closed