Upper Closure in Ordered Subset is Intersection of Subset and Upper Closure

Theorem

Let $L = \left({S, \preceq}\right)$ be an ordered set.

Let $\left({T, \precsim}\right)$ be an ordered subset of $L$.

Let $t \in T$.

Then $t^\succsim = T \cap t^\succeq$

Proof

By definition of ordered subset:

$T \subseteq S$

We will prove that

$t^\succsim \subseteq T \cap t^\succeq$

Let $x \in t^\succsim$

By definition of upper closure of element:

$x \in T$ and $t \precsim x$

By definition of ordered subset:

$t \preceq x$

By definition of upper closure of element:

$x \in t^\succeq$

Thus by definition of intersection:

$x \in T \cap t^\succeq$

$\Box$

We will prove that

$T \cap t^\succeq \subseteq t^\succsim$

Let $x \in T \cap t^\succeq$

By definition of intersection:

$x \in T$ and $x \in t^\succeq$

By definition of upper closure of element:

$t \preceq x$

By definition of ordered subset:

$t \precsim x$

Thus by definition of upper closure of element:

$x \in t^\succsim$

$\Box$

By definition of set equality:

$t^\succsim = T \cap t^\succeq$

$\blacksquare$