for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open