Proposition 4.7.1.35. Let $(S, \preceq )$ be a well-founded partially ordered set. Then there exists a well-ordering $\leq $ on $S$ which refines $\preceq $ in the following sense: for every pair of elements $s,t \in S$ satisfying $s \preceq t$, we also have $s \leq t$.
Proof. Let $Q$ denote the set of ordered pairs $(T, \leq _{T})$, where $T$ is a subset of $S$ which is closed downward with respect to $\preceq $ and $\leq _{T}$ is a well-ordering of $T$ which refines $\preceq $. We regard $Q$ as a partially ordered set, where $(T, \leq _{T} ) \leq (T', \leq _{T'} )$ if $T$ is an initial segment of $T'$ (with respect to the ordering $\leq _{T'}$), and the ordering $\leq _{T}$ coincides with the restriction of $\leq _{T'}$. The partially ordered set $Q$ satisfies the hypotheses of Zorn's lemma, and therefore contains a maximal element $( T_{\mathrm{max}}, \leq _{ T_{\mathrm{max}} } )$. To complete the proof, it will suffice to show that $T_{\mathrm{max}} = S$. Suppose otherwise. Then the set $S \setminus T_{\mathrm{max}}$ is nonempty, and therefore contains an element $s$ which is minimal with respect to the ordering $\preceq $. Set $T' = T_{\mathrm{max}} \cup \{ s\} $, and extend $\leq _{ T_{\mathrm{max}} }$ to a linear ordering $\leq _{T'}$ of $T'$ by declaring $s$ to be a largest element. Then $(T', \leq _{T'} )$ is an element of $Q$, contradicting the maximality of the pair $( T_{\mathrm{max}}, \leq _{ T_{\mathrm{max}} } )$. $\square$