for T being up-complete Scott TopLattice
for x being Element of T holds (downarrow x) ` is open