theorem Th11: :: WAYBEL11:11

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;