# Not Preceding implies There Exists Meet Irreducible Element Not Preceding

## Theorem

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.

Let $x, y \in S$ such that

$y \npreceq x$

Then

$\exists p \in S: p$ is meet irreducible and $x \preceq p$ and $y \npreceq p$

## Proof

By definition of continuous:

$L$ satisfies axiom of approximation

and

$\forall x \in S: x^\ll$ is directed.
$\exists u \in S: u \ll y \land u \npreceq x$
there exists way below open filter $F$ in $L$: $y \in F \subseteq u^\gg$
$u^\gg \subseteq u^\succeq$

By definition of upper set:

$x \notin F$

By definition of relative complement:

$x \in \complement_S\left({F}\right)$
$\exists m \in \complement_S\left({F}\right): x \preceq m \land m = \max \complement_S\left({F}\right)$
$m$ is meet irreducible.

Thus

$x \preceq m$

Aiming for a contradiction suppose that

$y \preceq m$

By definition of upper set:

$m \in F$

This contradicts $m \in \complement_S\left({F}\right)$ by definition of greatest element.

$\blacksquare$