Check the existence theorem on page 23 (I'm looking at the paper edition): "Let R be the ordered field of real numbers. There is an ordered field extension R* o

Check the existence theorem on page 23 (I'm looking at the paper edition): "Let R be the ordered field of real numbers. There is an ordered field extension R* of R and a mapping * from real functions to hyperreal functions (i.e., functions on R*) such that Axioms A - D hold." Note that he just starts with the reals. The actual definition of R* is in the middle of the proof: R* = {tau[epsilon] : tau(x) is an element of T(M)} Note that the proof uses Zorn's lemma, so it's definitely not "constructive" in the strict sense (in case that's what you meant).