**König's lemma** is a theorem in graph theory. It states that

ifGis a connected graph with infinitely many vertices such that every vertex has finite degree (= number of immediately adjacent vertices), then every vertex ofGis part of an infinitely long simple path.

A common special case of this is that every tree that contains infinitely many vertices, each having finite degree, has at least one infinite simple path.

Note that the vertex degrees have to be finite, but not bounded: it is possible to have one vertex of degree 10, another of degree 100, a third of degree 1000 *etc.*

The proof proceeds as follows. Start with the given vertex *v*_{1}. Every one of the infinitely many vertices of *G* can be reached from *v*_{1} with a simple path, and each such path must start with one of the finitely many vertices adjacent to *v*_{1}. So there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it *v*_{2}. Now, infinitely many vertices of *G* can be reached from *v*_{2} with a simple path which doesn't use the vertex *v*_{1}. Each such path must start with one of the finitely many vertices adjacent to *v*_{2}. So there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it *v*_{3}. Continuing in this fashion, an infinite simple path can be constructed (by mathematical induction).

One should note that this proof is not constructive, since it involves a proof by contradiction to establish that there exists an adjacent vertex from which infinitely many other vertices can be reached. Indeed the theorem cannot be proven in a constructive way.

The Mizar project has completely formalized and automatically checked the proof of a version of König's lemma in the file TREES_2.