König's Lemma/Proof 1
Take any vertex of $G$ and call it $v_1$.
Let $\PP_1$ be the set of all paths from $v_1$.
Each element of $\PP_1$ must start with an edge joining $v_1$ to some element of $\VV_1$.
There must be some $v_r \in \VV_1$ such that there is an infinite path from $v_r$ in $G$ which does not pass through $v_1$. Otherwise, every path from $v_1$ would be finite, and since there is a path from $v_1$ to each other vertex of the graph, all vertices are contained within one of these finite paths. There are a finite number of paths from $v_1$, so all vertices of $G$ are contained within a finite set of finite sets, contradicting the assumption that $G$ is infinite.
Each such infinite path must start with one of the elements of $\VV_2$.
Repeating the above argument shows that there is some $v_s \in \VV_2$ such that there is an infinite path from $v_s$ in $G$ which does not pass through $v_2$.
The result of this induction argument is that for all $n$ we can choose a vertex $v_n$ as per the construction.
The set of vertices chosen in the construction is then a path, because each one was chosen to be adjacent to the previous one, and the construction guarantees that the same vertex is never chosen twice.
Axiom:Axiom of Countable Choice for Finite Sets
This theorem depends on Axiom:Axiom of Countable Choice for Finite Sets.
As such, mathematicians are generally convinced of its truth and believe that it should be generally accepted.
Source of Name
This entry was named for Dénes Kőnig.