I was about to ask how he proves that, but that way lies an infinite regress, so I found a copy and checked. I see that he defines (without using the terminology) the real numbers to be the completion of the rational numbers for the usual Archimedean metric and so, as you say, is able to prove the completeness rather than postulating it. (This explains to me your remark elsethread (https://news.ycombinator.com/item?id=22712940) that "So this is … a case of 'what is a theorem if you have a model is only an axiom if you don't'.", which I didn't understand on first reading.)

Note that this is just a difference of terminology from other approaches; those approaches prove properties of an abstract object satisfying certain axioms, and then are obliged to exhibit a specific such object. The approach you favour is definitely more hands-on, but runs the risk of obscuring that really field axioms + uniqueness is all we need; if someone else prefers to construct their reals using, say, Dedekind cuts, then there is no need to check all the theorems proven along the way, only that the axioms of a complete (as an ordered or metric space) ordered field still hold.