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