Upper Closure of Element without Element is Filter implies Element is Meet Irreducible

Theorem

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

Let $x \in S$.

Let

$x^\succeq \setminus \set x$ be a filter in $L$.

Let $a, b \in S$.

Aiming for a contradiction, suppose:

$x = a \wedge b$ and $x \ne a$ and $x \ne b$

$x \preceq b$ and $x \preceq a$

$b, a \in x^\succeq$

By definitions of singleton and difference:

$b, a \in x^\succeq \setminus \set x$

By definition of filtered:

$\exists z \in x^\succeq \setminus \set x: z \preceq a \land z \preceq b$

By definition of infimum:

$z \preceq x$

By definition of upper section:

$x \in x^\succeq \setminus \set x$

Thus this contradicts $x \in \set x$ by definition of singleton.

$\blacksquare$