Proof that ZF set theory implies Weak König's Lemma In some of my other questions and in several references one finds the statement that 

ZF axioms imply WKL 

I have searched for the proof of this, but I so far cannot find a proof. I am looking for a proof not because I doubt it, but because I would like to know for sure which axioms are used in this proof.
I suspect that it may result from the underlying use of 2-valued logic (in ZF set theory) rather than any specific collection of ZF axioms, but I have not seen the proof to be sure.
Does anyone know where to find a proof that I can study?
 A: This is a trivial observation.

Suppose that $T=\{t_n\mid n\in\omega\}$ is a tree without any terminal nodes. Then $T$ has a branch.

Proof. Without loss of generality $t_0$ is the root of the tree. Now by induction let $f(0)=t_0$ and $f(n+1)=t_k$ if and only if $k=\min\{m\mid t_m\text{ is an immediate successor of }t_n\}$. Now $\{f(n)\mid n\in\omega\}$ is a branch. $\square$
In particular, a countable tree where every level is finite has an infinite branch.
And note that we didn't use any contradiction, or $2$-valued assumptions here. Since the well-ordering is given (and when it doesn't, we can instantiate the existential quantifier which assures that it does), we only have to "traverse" up the tree and pick the right node at each step.
So in order to not prove this, you'd have to be incapable of proving certain induction arguments.

This is not true that $\sf ZF$ proves this statement when $T$ is not countable from the beginning. An example of that is when consider a countable family of [non-empty] finite sets which does not admit a choice function $\{A_n\mid n\in\omega\}$, then the tree whose underlying set is $\bigcup_{n\in\omega}\prod_{k<n}A_k$ ordered by inclusion, is a counterexample.
