theorem Th39: :: WAYBEL12:39

for L being lower-bounded continuous LATTICE
for D being non empty countable dense Subset of L
for u being Element of L st u <> Bottom L holds
ex p being irreducible Element of L st
( p <> Top L & not p in uparrow ({u} "/\" D) )