theorem Th16: :: WAYBEL30:16

for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x