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

let x be Element of T; :: thesis: downarrow x is closed

Cl {x} = downarrow x by Lm2;

hence downarrow x is closed ; :: thesis: verum