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