plane defines a graph in which each face is bounded by at least three edges, and each edge bounds two faces; so, double counting gives the additional inequality . Using this inequality to eliminate from the Euler characteristic leads to the inequality . But if every vertex in the arrangement were the crossing point of three or more lines, then the total number of edges would be at least , contradicting this inequality. Therefore, some vertices must be the crossing point of only two lines, and as Melchior's more careful analysis shows, at least three ordinary vertices are needed in order to satisfy the inequality . As note, the same argument for the existence of an ordinary vertex was also given in 1944 by Norman Steenrod, who explicitly applied it to the dual ordinary line problem. Melchior's inequality By a similar argument, Melchior was able to prove a more general result. For every , let be the number of points to which lines are incident. Then or equivalently, Axiomatics writes of Kelly's proof that its use of Euclidean distance is unnecessarily powerful, "like using a sledge hammer to crack an almond". Instead, Coxeter gave another proof of the Sylvester–Gallai theorem within ordered geometry, an axiomatization of geometry in terms of betweenness that includes not only Euclidean geometry but several other related geometries. Coxeter's proof is a variation of an earlier proof given by Steinberg in 1944. The problem of finding a minimal set of axioms needed to prove the theorem belongs to reverse mathematics; see for a study of this question. The usual statement of the Sylvester–Gallai theorem is not valid in constructive analysis, as it implies the lesser limited principle of omniscience, a weakened form of the law of excluded middle that is rejected as an axiom of constructive mathematics. Nevertheless, it is possible to formulate a version of the Sylvester–Gallai theorem that is valid within the axioms of constructive analysis, and to adapt Kelly's proof of the theorem to be a valid proof under these axioms. Finding an ordinary line Kelly's proof of the existence of an ordinary line can be turned into an algorithm that finds an ordinary line by searching for the closest pair of a point and a line through two other points. report the time for this closest-pair search as , based on a brute-force search of all triples of points, but an algorithm