[proofplan] We prove the result by induction on the number of vertices. The key point is that every nonempty finite directed acyclic graph has a source, meaning a vertex with no incoming edge; otherwise repeatedly following incoming edges forces a repeated vertex and hence a directed cycle. After choosing a source, we delete it, topologically order the remaining induced subgraph by the induction hypothesis, and place the source first. [/proofplan]

[step:Prove that every nonempty finite directed acyclic graph has a source]Let $G=(V,E)$ be a nonempty finite directed acyclic graph. A source in $G$ means a vertex $s\in V$ such that there is no vertex $w\in V$ with $(w,s)\in E$. We claim that $G$ has a source. Suppose, to the contrary, that $G$ has no source. Then for every vertex $v\in V$ there exists a vertex $w\in V$ such that $(w,v)\in E$. Choose a vertex $v_0\in V$. Since $v_0$ is not a source, choose $v_1\in V$ with $(v_1,v_0)\in E$. Continuing recursively, for each integer $k\geq 1$ choose $v_k\in V$ such that $(v_k,v_{k-1})\in E$. Let $n=|V|$. The finite list $v_0,v_1,\dots,v_n$ contains $n+1$ vertices of the finite set $V$, so two entries coincide. Choose indices $0\leq i<j\leq n$ with $v_i=v_j$ and with $j-i$ minimal among all such coincidences. By minimality, the vertices $v_i,v_{i+1},\dots,v_{j-1}$ are pairwise distinct. The edges $(v_j,v_{j-1}),(v_{j-1},v_{j-2}),\dots,(v_{i+1},v_i)$ form a directed cycle because $v_j=v_i$. This contradicts that $G$ is acyclic. Therefore $G$ has a source.[/step]

[guided]The only nontrivial ingredient in the induction is the existence of a vertex with no incoming edge. We prove it directly. Let $G=(V,E)$ be a nonempty finite directed acyclic graph. A source is a vertex $s\in V$ for which no directed edge enters $s$, meaning there is no $w\in V$ satisfying $(w,s)\in E$. Assume for contradiction that no source exists. Then every vertex has at least one incoming edge. Choose an initial vertex $v_0\in V$. Since $v_0$ is not a source, there exists $v_1\in V$ such that $(v_1,v_0)\in E$. Since $v_1$ is also not a source, there exists $v_2\in V$ such that $(v_2,v_1)\in E$. Repeating this construction gives a sequence of vertices $(v_k)_{k\geq 0}$ with \begin{align*} (v_k,v_{k-1})\in E \end{align*} for every integer $k\geq 1$. Now use finiteness. Let $n=|V|$. The list $v_0,v_1,\dots,v_n$ has $n+1$ entries but takes values in a set with only $n$ elements. Hence some two entries are equal. Choose $0\leq i<j\leq n$ such that $v_i=v_j$ and $j-i$ is as small as possible. This minimality ensures that $v_i,v_{i+1},\dots,v_{j-1}$ are pairwise distinct; if two of them repeated earlier, we would have found a shorter repetition. The directed edges were constructed in the backward direction: \begin{align*} (v_j,v_{j-1})\in E,\quad (v_{j-1},v_{j-2})\in E,\quad \dots,\quad (v_{i+1},v_i)\in E. \end{align*} Since $v_j=v_i$, these edges form a directed cycle starting at $v_j$, moving through $v_{j-1},\dots,v_{i+1}$, and returning to $v_i=v_j$. This contradicts the assumption that $G$ is a directed acyclic graph. Therefore the assumption that no source exists is false, and $G$ has a source.[/guided]

[step:Handle the empty graph and set up induction on the number of vertices] We prove the theorem by induction on $n=|V|$. If $n=0$, then $V=\varnothing$. The empty relation on $\varnothing$ is a total order, and there are no edges to check. Thus it is a topological order. Assume now that $n\geq 1$ and that every finite directed acyclic graph with $n-1$ vertices has a topological order. [/step]

[step:Delete a source and topologically order the remaining induced subgraph] Let $G=(V,E)$ be a finite directed acyclic graph with $|V|=n$. By the source lemma proved above, choose a source $s\in V$. Define $V'=V\setminus\{s\}$ and define the induced edge set \begin{align*} E' := E\cap (V'\times V'). \end{align*} Let $G'=(V',E')$. The graph $G'$ is finite and has $n-1$ vertices. It is also acyclic, because any directed cycle in $G'$ would be a directed cycle in $G$. Hence the induction hypothesis gives a total order $\prec'$ on $V'$ such that, for every $(u,v)\in E'$, one has $u\prec' v$. [/step]

[step:Place the source first and verify that every edge points forward] Define a relation $\prec$ on $V$ as follows. For vertices $x,y\in V$, set $x\prec y$ if either $x=s$ and $y\in V'$, or $x,y\in V'$ and $x\prec' y$. Together with equality, this gives a total order on $V$: the vertex $s$ is first, and all remaining vertices are ordered by $\prec'$. It remains to check the edge condition. Let $(u,v)\in E$. If $v=s$, then $(u,s)\in E$, contradicting that $s$ is a source. Hence $v\neq s$. If $u=s$, then $s\prec v$ by definition of $\prec$. If $u\neq s$, then $u,v\in V'$, so $(u,v)\in E'$, and the induction hypothesis gives $u\prec' v$, hence $u\prec v$. Thus every directed edge $(u,v)\in E$ satisfies $u\prec v$. Therefore $\prec$ is a topological order of $G$, completing the induction and the proof. [/step]