Not Preceding implies Approximating Relation and not Preceding

From ProofWiki
Jump to navigation Jump to search


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$.


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


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$