subgraph to require more than colors). The binary relation of nonadjacency in is an equivalence relation, and its equivalence classes provide a -coloring of . However, this proof is more difficult to generalize than the compactness proof. The theorem can also be proved using ultrafilters or non-standard analysis. gives a proof for graphs with a countable number of vertices based on Kőnig's infinity lemma. Dependence on choice All proofs of the De Bruijn–Erdős theorem use some form of the axiom of choice. Some form of this assumption is necessary, as there exist models of mathematics in which both the axiom of choice and the De Bruijn–Erdős theorem are false. More precisely, showed that the theorem is a consequence of the Boolean prime ideal theorem, a property that is implied by the axiom of choice but weaker than the full axiom of choice, and showed that the De Bruijn–Erdős theorem and the Boolean prime ideal theorem are equivalent in axiomatic power. The De Bruijn–Erdős theorem for countable graphs can also be shown to be equivalent in axiomatic power, within a theory of second-order arithmetic, to Kőnig's infinity lemma. For a counterexample to the theorem in models of set theory without choice, let be an infinite graph in which the vertices represent all possible real numbers. In , connect each two real numbers and by an edge whenever one of the values is a rational number. Equivalently, in this graph, edges exist between all real numbers and all real numbers of the form , for rational numbers . Each path in this graph, starting from any real number , alternates between numbers that differ from by a rational number plus an even multiple of and numbers that differ from by a rational number plus an odd multiple of . This alternation prevents from containing any cycles of odd length, so each of its finite subgraphs requires only two colors. However, in the Solovay model in which every set of real numbers is Lebesgue measurable, requires infinitely many colors, since in this case each color class must be a measurable set and it can be shown that every measurable set of real numbers with no edges in must have measure zero. Therefore, in the Solovay model, the (infinite) chromatic number of all of is much larger than the chromatic number of its finite subgraphs (at most two). Generalizations proves the following theorem, which