A topological criterion for type completeness of definably complete ordered fields

A first order expansion M = (M, ,+, ·, 0, 1, . . . ) of an ordered field is said to be definably complete if every bounded definable subset of M has a least upper bound in M. These structures which are first order versions of Dedekind complete ordered fields, satisfy definable versions of many topological properties of the reals. On the other hand, type completeness of ordered structures which was introduced in [6], is a first order property that make the definably complete structures to be further similar to the real ordered field. Here, we provide a topological criterion for type completeness of definably complete ordered fields