for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds downarrow x is closed by Th8, Th7;