Preceding implies Inclusion of Segments of Auxiliary Relation

From ProofWiki
Jump to: navigation, search

Theorem

Let $\left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.

Let $R$ be an auxiliary relation on $S$.

Let $x, y \in S$ such that

$x \preceq y$


Then

$x^R \subseteq y^R$

where $x^R$ denotes the $R$-segment of $x$.


Proof

Let $a \in x^R$.

By definition of $R$-segment of $x$:

$\left({a, x}\right) \in R$

By definition of reflexivity:

$a \preceq a$

By definition of auxiliary relation:

$\left({a, y}\right) \in R$

Thus by definition of $R$-segment of $y$:

$a \in y^R$

$\blacksquare$


Sources