Does this theorem have a name, and where can I find a proof? "Every finite, weakly connected digraph contains at least one source or cycle." I am looking for a proof of a particular theorem. The theorem would state:

Every finite, weakly connected digraph contains at least one source or cycle.

Since every finite graph is either cyclic or acyclic, an alternative statement would be:

Every finite, weakly connected, acyclic digraph has a source.

with the previous theorem as a corollary.
Note: Assuming that the above is correct, then for any natural number $n$, an effective procedure exists to show that every weakly connected, acyclic digraph with fewer than $n$ vertices has a source - namely, "pick a point and backtrack". While this makes the theorem seem trivial, it is insufficient to prove that every finite, weakly connected, acyclic digraph has a source, hence the request for a proof.

I checked the library, all of my textbooks, and searched online, but I can't seem to find any reference to this theorem. The notion seems sufficiently obvious so as to be a fundamental result in graph theory, but no one I've spoken to has been able to put a name to it.
Is there a name for this theorem (or other, more significant theorem from which it can be easily derived), and where can I find a proof of it?
 A: I don't know of a particular name for the theorem, but the idea of "pick a point and backtrack" is pretty much a proof - you can formalize it as follows, by proving the contrapositive:

Let $G$ be a finite non-empty directed graph, none of which is a source. Then $G$ is cyclic.

Then to prove it, let $n$ be the number of vertices and let $x_0$ be an arbitrary vertex. Choose a sequence $x_1,\ldots,x_n$ with the property that $x_i$ has an edge to $x_{i-1}$. This is possible since there are no sources. However, now we have a sequence $x_0,\ldots,x_n$ with $n+1$ elements, thus by the pigeonhole principle, some pair must be the same - that is $x_i=x_j$ for some $j\neq i$. Assume without loss of generality that $i>j$. Then $$x_i\rightarrow x_{i-1} \rightarrow \ldots \rightarrow x_{j+1} \rightarrow x_j$$
is a cycle*.
(*If you insist upon a simple cycle, you can choose the a $(i,j)$ with $x_i=x_j$ and $i\neq j$ that minimizes $|i-j|$, since we know that the set of such pairs is non-empty)
A: The digraph doesn't even need to be weakly connected, just non-empty.
Let $W$ be a directed walk in the digraph $D$ of maximal length.  (As $D$ is acyclic, the length of directed walks is bounded above by the number of nodes in $D$, so this is a valid construction.)  Consider $v$, the origin of $W$.  Since $D$ is acyclic, $D$ does not have an arc with $v$ as its tail whose head is another vertex in $W$.  Since $W$ is of maximal length, $D$ does not have an arc with $v$ as its tail whose head is vertex not in $W$.  Therefore, $v$ is a source.
