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 )
A1: downarrow x is closed by Th38;
A2: {x} is closed by Th38;
uparrow x is closed by Th38;
hence ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) by A1, A2; :: thesis: verum