theorem Th34: :: WAYBEL12:34

for L being lower-bounded continuous LATTICE
for V being upper Open Subset of L
for N being non empty countable Subset of L
for v being Element of L st V "/\" N c= V & v in V holds
ex O being Open Filter of L st
( {v} "/\" N c= O & O c= V & v in O )