for T being complete Lawson TopLattice
for X being finite Subset of T holds
( (uparrow X) ` is open & (downarrow X) ` is open )