for L being lower-bounded algebraic LATTICE
for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is completely-irreducible & x <= p & not y <= p )