# Not Preceding implies Approximating Relation and not Preceding

 It has been suggested that this article or section be renamed: It's tough to suggest an alternative, but this title doesn't cut it. One may discuss this suggestion on the talk page.

## Theorem

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

Let $x, y \in S$ such that

$x \npreceq y$

Let $\mathcal R$ be an approximating relation on $S$.

Then

$\exists u \in S: \left({u, x}\right) \in \mathcal R \land u \npreceq y$

## Proof

By definition of approximating relation:

$x = \sup \left({x^{\mathcal R} }\right)$

By definition of supremum:

$y$ is upper bound for $x^{\mathcal R} \implies x \preceq y$

By definition of upper bound:

$\exists u \in S: u \in x^{\mathcal R} \land u \npreceq y$

Thus by definition of $\mathcal R$-segment:

$\exists u \in S: \left({u, x}\right) \in \mathcal R \land u \npreceq y$

$\blacksquare$