Not Preceding implies Exists Completely Irreducible Element in Algebraic Lattice

Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.

Let $x, y \in S$ such that

$y \npreceq x$

Then

$\exists p \in S: p$ is completely irreducible $\land ~x \preceq p \land y \npreceq p$

Proof

By definition of algebraic:

$\forall z \in S: z^\ll$ is directed

and

$L$ satisfies axiom of approximation.
$\exists k \in S: k \ll y \land k \npreceq x$
$\exists z \in K\left({L}\right): k \preceq z \preceq y$

By definition of transitivity:

$z \npreceq x$

By definition of upper closure of element:

$x \notin z^\succeq$

By definition of difference:

$x \in S \setminus z^\succeq$

By definition of relative complement:

$x \in \complement_S\left({z^\succeq}\right)$

By definition of compact subset:

$z$ is a compact element.
$z^\succeq$ is a way below open filter on $L$.
$\exists p \in S: x \preceq p \land p = \max\complement_S\left({z^\succeq}\right)$
$p$ is completely irreducible.

Thus $x \preceq p$

Aiming for a contradiction suppose that

$y \preceq p$

By definition of transitivity:

$z \preceq p$

By definition of maximum element:

$p \in \complement_S\left({z^\succeq}\right)$

By definition of relative complement:

$p \notin z^\succeq$

Thus this contradicts $z \preceq p$ by definition of upper closure of element.

$\blacksquare$