In Hilbert's Foundations of Geometry, the axiom of completeness is presented as follows:
To a system of points, straight lines, and planes, it is impossible to add other elements in such a manner that the system thus generalized shall form a new geometry obeying all of the five groups of axioms. In other words, the elements of geometry form a system which is not susceptible of extension, if we regard the five groups of axioms as valid.
He goes on to assert that this can be used to prove "Bolzano's theorem," that every bounded sequence of points has a limit point.
I've been puzzling over this axiom for some time: this implication seems harder the more I look at it. Obviously, we want to suppose there is a sequence with no limit point and construct an extension that includes one. But Hilbert's axioms do not have a dimension bound (unlike Tarski's, say) so as far as I know there can be infinite-dimensional models. That seems to rule out the trivial "show that it is a submodel of a Cartesian model over real numbers."
If that trick doesn't work, we must construct the extension explicitly. But this is no easy task; a new point can intersect at most one pre-existing line, and a new line can intersect at most one pre-existing point. Likewise for points and planes, with "at most two" instead. So we're going to be adding a lot of new objects, with many new relations between them. And, we need to do this in such a way that the axioms of geometry continue to hold once we are done.
I've been unable to find any literature that does this construction. Many sources replace this form of completeness with a Dedekind cut or Cantor nested intervals formulation, probably due to the complexity of this task. I would appreciate any guidance or references for this proof.