If Element Does Not Belong to Ideal then There Exists Prime Ideal Including Ideal and Excluding Element

Theorem

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

Let $I$ be an ideal in $L$.

Let $x$ be an element of $S$.

Suppose $x \notin I$

Then there exists a prime ideal $P$ in $L$: $I \subseteq P$ and $x \notin P$

$x^\succeq$ is a filter.

We will prove that

$I \cap x^\succeq = \O$

Aiming for a contradiction, suppose:

$\exists y: y \in I \cap x^\succeq$

By definition of intersection:

$y \in I$ and $y \in x^\succeq$

$x \preceq y$

By definition of lower section:

$x \in I$

This contradicts $x \notin I$

$\Box$

there exists a prime ideal $P$ in $L$: $I \subseteq P$ and $P \cap x^\succeq = \O$

By definition of reflexivity:

$x \preceq x$

$x \in x^\succeq$

Thus by definitions of intersection and empty set:

$x \notin P$

$\blacksquare$