let T be up-complete Scott TopLattice; :: thesis: for x being Element of T holds downarrow x is closed
let x be Element of T; :: thesis: downarrow x is closed
Cl {x} = downarrow x by Lm2;
hence downarrow x is closed ; :: thesis: verum