Thus "f" gives a bound for how “wide” the tree is. The following basis theorems apply to infinite, computably bounded, computable subtrees of formula_16. A weak form of Kőnig's lemma which states that every infinite binary tree has an infinite branch is used to define the subsystem WKL0 of second-order arithmetic. This subsystem has an important role in reverse mathematics. Here a binary tree is one in which every term of every sequence in the tree is 0 or 1, which is to say the tree is computably bounded via the constant function 2. The full form of Kőnig's lemma is not provable in WKL0, but is equivalent to the stronger subsystem ACA0. The proof given above is not generally considered to be constructive, because at each step it uses a proof by contradiction to establish that there exists an adjacent vertex from which infinitely many other vertices can be reached, and because of the reliance on a weak form of the axiom of choice. Facts about the computational aspects of the lemma suggest that no proof can be given that would be considered constructive by the main schools of constructive mathematics. The fan theorem of is, from a classical point of view, the contrapositive of a form of Kőnig's lemma. A subset "S" of formula_19 is called a "bar" if any function from formula_2 to the set formula_21 has some initial segment in "S". A bar is "detachable" if every sequence is either in the bar or not in the bar (this assumption is required because the theorem is ordinarily considered in situations where the law of the excluded middle is not assumed). A bar is "uniform" if there is some number "N" so that any function from formula_2 to formula_21 has an initial segment in the bar of length no more than formula_24. Brouwer's fan theorem says that any detachable bar is uniform. This can be proven in a classical setting by considering the bar as an open covering of the compact topological space formula_25. Each sequence in the bar represents a basic open set of this space, and these basic open sets cover the space by assumption. By compactness, this cover has a finite subcover. The "N" of the fan theorem can be taken to be the length of the longest sequence whose basic open set is in the finite subcover. This topological proof can be used in classical mathematics to show that the following form of Kőnig's lemma holds: for any natural number "k", any infinite subtree of the tree formula_26 has an infinite path.