Set Coarser than Upper Section is Subset

Theorem

Let $\struct {S, \preceq}$ be a preordered set.

Let $A, B$ be subsets of $S$ such that

$A$ is coarser than $B$

and

$B$ is an upper section.

Then:

$A \subseteq B$

Proof

Let $x \in A$.

By definition of coarser subset:

$\exists y \in B: y \preceq x$

Thus by definition of upper section:

$x \in B$

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article YELLOW_4:8