for T being complete Lawson TopLattice
for x being Element of T holds
( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )