theorem Th35: :: WAYBEL12:35

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 x, y being Element of L st V "/\" N c= V & y in V & not x in V holds
ex p being irreducible Element of L st
( x <= p & not p in uparrow ({y} "/\" N) )