# Preceding implies if Less Upper Bound then Greater Upper Bound

Jump to navigation
Jump to search

## Theorem

Let $L = \struct {S, \preceq}$ be an ordered set.

Let $x, y \in S$ such that

- $x \preceq y$

Let $X \subseteq S$.

Then

- $x$ is upper bound for $X \implies y$ is upper bound for $X$

and

- $y$ is lower bound for $X \implies x$ is lower bound for $X$.

## Proof

### First Implication

Let $x$ be upper bound for $X$,

Let $z \in X$.

By definition of upper bound:

- $z \preceq x$

Thus by definition of transitivity:

- $z \preceq y$

$\Box$

### Second Implication

This follows by mutatis mutandis.

$\blacksquare$

## Sources

- Mizar article YELLOW_0:4