# Completely Irreducible and Subset Admits Infimum Equals Element implies Element Belongs to Subset

## Theorem

Let $L = \struct {S, \preceq}$ be an ordered set.

Let $x \in S$ such that

$x$ is completely irreducible.

Let $X \subseteq S$ such that

$X$ admits an infimum and $x = \inf X$

Then $x \in X$

## Proof

$x \notin X$
$\exists q \in S: x \prec q \land \left({\forall s \in S: x \prec s \implies q \preceq s}\right) \land x^\succeq = \left\{ {x}\right\} \cup q^\succeq$

where $x^\succeq$ denotes the upper closure of $x$.

We will prove that

$X \subseteq q^\succeq$

Let $y \in X$.

By definitions of infimum and lower bound:

$x \preceq y$

By definition of strictly precede:

$x \prec y$

By existence of $q$:

$q \preceq y$

Thus by definition of upper closure of element:

$y \in q^\succeq$

$\Box$

$\inf\left({q^\succeq}\right) = q$
$q \preceq x$

Thus this contrsdicts $x \prec q$

$\blacksquare$