theorem :: WAYBEL11:14

for T being complete Scott TopLattice
for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )