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 an $M$-definable continuous embedding $f:(a,b)\to X$). It is said to be completable if $\lim_{x\downarrow a}f(x)$ and $\lim_{x \uparrow b}f(x)$ exist.)
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 on $X$ has a limit in $X$. An $M$-definable type is a homomorphism 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)$. An $M$-definable type defines a complete $n$-type 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?
