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$X$ means that any M$M$-definable curve in X$X$ is completable. (a curve in X$X$ is a Man $M$-definable continuous embedding f:(a,b)→X$f:(a,b)\to X$). It is said to be completable if $lim_{x\downarrow a}f(x)$$\lim_{x\downarrow a}f(x)$ and $lim_{x \uparrow b}f(x)$ exists$\lim_{x \uparrow b}f(x)$ exist.)
In a lecture course at Paris VI, I saw another definition of definable compactness: X$X$ is definable compact if and only if any M$M$-definable type sur Xon $X$ has a limit in X$X$. An M$M$-definable type is a homomorphismushomomorphism of booleanBoolean algebras $d_x$ from the booleanBoolean algebra of all first-order formulas in a language L$L$ to the booleanBoolean algebra of all first-order formulas in the language L(M)$L(M)$. A MAn $M$-definable type defines a ncomplete $n$-type complet on X$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?
