let R be complete connected LATTICE; :: thesis: for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open
let T be Scott TopAugmentation of R; :: thesis: for x being Element of T holds (downarrow x) ` is open
let x be Element of T; :: thesis: (downarrow x) ` is open
reconsider S = downarrow x as lower directly_closed Subset of T by WAYBEL11:8;
S ` is open ;
hence (downarrow x) ` is open ; :: thesis: verum