# 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.

By Axiom of Approximation in Up-Complete Semilattice:

- $\exists k \in S: k \ll y \land k \npreceq x$

By Algebraic iff Continuous and For Every Way Below Exists Compact Between:

- $\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.

By Upper Closure of Element is Way Below Open Filter iff Element is Compact:

- $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)$

Thus by Maximal implies Completely Irreducible:

- $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$

## Sources

- Mizar article WAYBEL16:31