König's lemma states that every finitely branching infinite tree has an infinite branch.

To prove this we show how such an infinite branch can be constructed.
Starting at the root, `t`

, we construct a branch,
_{0}`t`

, _{0}`t`

, ...,
so that every _{1}`t`

in the sequence has infinitely many descendants.
Since the tree is finitely branching, and the finite union of finite sets is finite,
then at least one child of the ultimate node in the sequence has infinitely many children and so this sequence can
always be extended.
_{i}

Doets, Kees. *From Logic to Logic Programming.* MIT Press, 1994.

Copyright © 2014 Barry Watson. All rights reserved.