let T be complete Lawson TopLattice; :: thesis: for x being Element of T holds
( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )
let x be Element of T; :: thesis: ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )
( uparrow x is closed & downarrow x is closed & {x} is closed ) by Th38;
hence ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) by TOPS_1:29; :: thesis: verum