let T be up-complete Scott TopLattice; :: thesis: for x being Element of T holds (downarrow x) ` is open
let x be Element of T; :: thesis: (downarrow x) ` is open
downarrow x is closed by Th11;
hence (downarrow x) ` is open ; :: thesis: verum