# Condition for Well-Foundedness/Forward Implication

Jump to navigation
Jump to search

## Theorem

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

Let $\struct {S, \preceq}$ be well-founded.

Then there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that $\forall n \in \N: a_{n + 1} \prec a_n$.

## Proof

Suppose there exists an infinite sequence $\sequence {a_n}$ in $S$ such that:

- $\forall n \in \N: a_{n + 1} \prec a_n$

We let $T = \set {a_0, a_1, a_2, \ldots}$.

Clearly $T$ has no minimal element.

Thus by definition $S$ is not well-founded.

$\blacksquare$

## Sources

- 1993: Keith Devlin:
*The Joy of Sets: Fundamentals of Contemporary Set Theory*(2nd ed.) ... (previous) ... (next): $\S 1$: Naive Set Theory: $\S 1.5$: Relations: Lemma $1.5.1$