for N being complete Lawson TopLattice
for X being Subset of N holds
( X in lambda N iff X is open ) by Th9;