theorem Th39: :: WAYBEL19:39

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