[proofplan] The strategy is a well-ordering argument on walks. Among all $x$–$y$ walks contained in $W$ — that is, subsequences of the vertex sequence of $W$ that themselves form an $x$–$y$ walk — we select one of minimum length, call it $W'$. We then show that $W'$ cannot contain a repeated vertex: a repetition would allow us to excise the segment between the two occurrences and obtain a strictly shorter $x$–$y$ subwalk, contradicting the minimality of $W'$. Since $W'$ has no repeated vertices and is an $x$–$y$ walk with $x \neq y$, it is by definition an $x$–$y$ path. [/proofplan]

[step:Extract a minimum-length $x$–$y$ subwalk of $W$]Write the walk $W$ as a finite sequence of vertices \begin{align*} W = w_0, w_1, w_2, \ldots, w_\ell, \end{align*} where $w_0 = x$, $w_\ell = y$, and $w_{i-1} w_i \in E(G)$ for every $1 \le i \le \ell$. Call a sequence $(w_{i_0}, w_{i_1}, \ldots, w_{i_k})$ with $0 \le i_0 < i_1 < \cdots < i_k \le \ell$ an **$x$–$y$ subwalk of $W$** if $w_{i_0} = x$, $w_{i_k} = y$, and $w_{i_{j-1}} w_{i_j} \in E(G)$ for every $1 \le j \le k$. The length of such a subwalk is $k$, the number of edges. The collection $\mathcal{S}$ of $x$–$y$ subwalks of $W$ is non-empty: $W$ itself is an $x$–$y$ subwalk of $W$ (take $i_j = j$). The length function $\mathcal{S} \to \mathbb{N}_0$ takes values in the non-negative integers, so by the well-ordering principle of $\mathbb{N}_0$ there exists an element $W' \in \mathcal{S}$ of minimum length. Write \begin{align*} W' = w'_0, w'_1, \ldots, w'_m, \end{align*} so $w'_0 = x$, $w'_m = y$, each $w'_{j-1} w'_j \in E(G)$, and $m$ is the minimum length in $\mathcal{S}$.[/step]

[guided]We must be careful about what "contains as a subsequence" means in the theorem statement. The walk $W$ is a finite sequence of vertices; an $x$–$y$ subwalk of $W$ is a choice of indices $0 \le i_0 < i_1 < \cdots < i_k \le \ell$ such that the induced subsequence $(w_{i_0}, w_{i_1}, \ldots, w_{i_k})$ starts at $x$, ends at $y$, and every consecutive pair is an edge in $G$. We are not allowed to reorder the vertices or insert new ones — only to skip some. The collection $\mathcal{S}$ of $x$–$y$ subwalks of $W$ is non-empty: taking $k = \ell$ and $i_j = j$ gives $W$ itself, which is an $x$–$y$ walk by hypothesis. The length of a subwalk (the number of edges) is a non-negative integer, and the well-ordering principle of $\mathbb{N}_0$ asserts that any non-empty subset of $\mathbb{N}_0$ has a least element. Apply this to the set of lengths of elements of $\mathcal{S}$: there exists a minimum length $m$, and therefore at least one subwalk $W' \in \mathcal{S}$ attaining it. Fix any such $W'$ and write \begin{align*} W' = w'_0, w'_1, \ldots, w'_m, \qquad w'_0 = x,\ w'_m = y,\ w'_{j-1} w'_j \in E(G). \end{align*} By the hypothesis $x \neq y$ we have $m \geq 1$: a subwalk of length $0$ would be the single vertex $x$, which cannot also equal $y$. The minimality property — there is no shorter $x$–$y$ subwalk of $W$ — is the only thing we will use about $W'$ in the next step. Everything else follows from it.[/guided]

[step:Derive a contradiction from any repeated vertex in $W'$]We claim that the vertices $w'_0, w'_1, \ldots, w'_m$ are pairwise distinct. Suppose for contradiction there exist indices $0 \le p < q \le m$ with $w'_p = w'_q$. Define the excision \begin{align*} W'' := w'_0, w'_1, \ldots, w'_p, w'_{q+1}, w'_{q+2}, \ldots, w'_m, \end{align*} obtained from $W'$ by deleting the segment $w'_{p+1}, \ldots, w'_q$. We check $W''$ is an $x$–$y$ subwalk of $W$ of length strictly less than $m$: 1. **Endpoints.** $W''$ starts with $w'_0 = x$ and ends with $w'_m = y$. 2. **Edges.** For $1 \le j \le p$, the pair $w'_{j-1} w'_j$ is an edge of $W'$, hence an edge of $G$. For $p+2 \le j \le m$, similarly $w'_{j-1} w'_j \in E(G)$. The only new adjacency introduced is at the splice point: the consecutive pair $w'_p, w'_{q+1}$. Since $w'_p = w'_q$, this pair equals $w'_q w'_{q+1}$, which is an edge of $W'$, hence an edge of $G$. (If $q = m$, the splice drops the tail entirely, so $W''$ ends at $w'_p = w'_q = w'_m = y$ with no splice edge to check.) 3. **Subsequence of $W$.** $W'$ is a subsequence of $W$ by construction, and $W''$ is a subsequence of $W'$ (we only deleted entries), so $W''$ is a subsequence of $W$. 4. **Length.** $W''$ has $m - (q - p)$ edges. Since $q > p$ we have $q - p \ge 1$, so the length of $W''$ is strictly less than $m$. Thus $W'' \in \mathcal{S}$ has length less than $m$, contradicting the minimality of $W'$.[/step]

[guided]The reason we took a **minimum-length** subwalk is exactly so that we could run an excision argument: any repetition gives us a way to shorten, and minimality forbids shortening, so repetitions are forbidden. Suppose for contradiction that $W'$ has a repeated vertex: there are indices $p < q$ in $\{0, 1, \ldots, m\}$ with $w'_p = w'_q$. Define \begin{align*} W'' := w'_0, w'_1, \ldots, w'_p, w'_{q+1}, w'_{q+2}, \ldots, w'_m. \end{align*} We have cut out the segment $w'_{p+1}, w'_{p+2}, \ldots, w'_q$ and stitched the remaining pieces at the common vertex. Why does this still form an $x$–$y$ walk? - The starting vertex of $W''$ is $w'_0 = x$ and the ending vertex is $w'_m = y$ (or $w'_p = w'_q = y$ in the boundary case $q = m$, which still gives endpoint $y$). - Every consecutive pair of vertices in $W''$, **except possibly the splice point**, is a consecutive pair in $W'$ and therefore an edge of $G$. At the splice point, the consecutive pair is $w'_p$ followed by $w'_{q+1}$. Now $w'_p = w'_q$, so this pair is literally the same two vertices as $w'_q, w'_{q+1}$, which is an edge of $W'$ (and hence of $G$). So $W''$ is an $x$–$y$ walk. Is it a subwalk of $W$? Yes: $W'$ was a subsequence of $W$ (a selection of indices into $W$), and $W''$ is obtained from $W'$ by dropping further entries, so $W''$ is also a subsequence of $W$ — a sub-subsequence is still a subsequence. How long is $W''$? We removed $q - p$ entries (namely $w'_{p+1}, \ldots, w'_q$), so $W''$ has $m + 1 - (q - p)$ vertices and therefore $m - (q - p)$ edges. Since $p < q$, we have $q - p \ge 1$, so $W''$ is strictly shorter than $W'$. We have constructed an $x$–$y$ subwalk of $W$ strictly shorter than $W'$. This contradicts the choice of $W'$ as a minimum-length such subwalk. The assumption of a repeated vertex therefore fails, so the vertices $w'_0, \ldots, w'_m$ are pairwise distinct.[/guided]

[step:Conclude that $W'$ is an $x$–$y$ path] An $x$–$y$ **path** in $G$ is an $x$–$y$ walk whose vertices are pairwise distinct. By the previous step, $W'$ has pairwise distinct vertices, and by construction $W'$ is an $x$–$y$ walk that is a subsequence of $W$. Hence $W'$ is an $x$–$y$ path contained in $W$ as a subsequence, as claimed. [/step]