for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }