= Solution
A relation $r$ on a set $a$ is a <well-founded relation> when every nonempty subset $b\subseteq a$ contains an element $y$ with no $x\in b$ satisfying $x\,r\,y$. The <well-founded recursion> theorem states that a rule assigning a value at $y$ from the already assigned values at its predecessors determines a unique function on $a$; the rule must give a unique set-valued output for every possible predecessor assignment. No choice or transitivity of $r$ is needed.
Apply recursion with
$$
f(y)=\sup\{f(x)+1:x\,r\,y\}.
$$
The empty supremum is zero. <Well-founded induction> makes every value an <ordinal>; the <Axiom schema of replacement> collects the values into a set. Choose an <ordinal> $\alpha$ larger than every value. Then $f:a\to\alpha$, and $x\,r\,y$ implies $f(x)+1\le f(y)$, hence $f(x)<f(y)$.
Conversely, suppose such an ordinal-valued function exists. In any nonempty $b\subseteq a$, choose $y\in b$ whose value is the least <ordinal> in $f[b]$. There can be no $x\in b$ with $x\,r\,y$, because it would have smaller value. Thus $r$ is well-founded, proving the equivalence.
Using the <axiom of choice>, fix a <well-order> $\prec$ of $a$. Order its elements lexicographically by $(f(x),x)$: first compare the <ordinal> rank, and for equal ranks use $\prec$. Every nonempty subset has a smallest rank and then a least element in that rank fibre, so this is a <well-order>. Since $x\,r\,y$ strictly increases rank, it respects every original relation pair. Hence \b[every <well-founded relation> extends to a <well-order> under choice].
Back to article page
