We have an o-minimal structure M with the order topology. $X \subseteq M^n$ with the induced topology. The article "Definable compactness and definable subgroups of o-minimal groups" by Steinhorn and Peterzil shows that $X \subseteq M^n$ is definable compact if and only if X is being bounded and closed.
Definable compactness of X means that any M-definable curve in X is completable. (a curve in X is a M-definable continuous embedding f:(a,b)→X). It is said to be completable if $lim_{x\downarrow a}f(x)$ and $lim_{x \uparrow b}f(x)$ exists.)
In a lecture course at Paris VI, I saw another definition of definable compactness: X is definable compact if and only if any M-definable type sur X has a limit in X. An M-definable type is a homomorphismus of boolean algebras $d_x$ from the boolean algebra of all first-order formulas in a language L to the boolean algebra of all first-order formulas in the language L(M). A M-definable type defines a n-type complet on X: $$p\vert_X = { \phi(x_1, \dots, x_n, b_1, \dots, b_m) \vert (b_1, \dots, b_m) \in B^m, M \models d_x \phi (b_1, \dots , b_m) } $$ A n-type $p$ is said to be on a definable set $X$, if the formule that defines X, is contained in $p$. Un n-type $p$ has $x \in M^n$ as limit, if for any definable neighborhood $V$ of $x$, $p$ is on $V$.
Why are these two definitions equivalent? I can't find anything on the second definition. Are there any sources easily accessible that explain that equivalence?
