Let $T$ be a complete $O$-minimal theory in a language $L$. We first give an elementary proof of the result (due to Marker and Steinhorn) that all types over Dedekind complete models of $T$ are definable. Let $L^\ast$ be $L$ together with a unary predicate $P$. Let $T^\ast$ be the $L^\ast$-theory of all pairs $(N, M)$, where $M$ is a Dedekind complete model of $T$ and $N$ is an $|M|^+$-saturated elementary extension of $N$ (and $M$ is the interpretation of $P$). Using the definability of types result, we show that $T^\ast$ is complete and we give a simple set of axioms for $T^\ast$. We also show that for every $L^\ast$-formula $\phi(\mathbf{x})$ there is an $L$-formula $\psi(\mathbf{x})$ such that $T^\ast \models (\forall \mathbf{x})(P(\mathbf{x}) \rightarrow (\phi(\mathbf{x}) \mapsto \psi (\mathbf{x}))$. This yields the following result: Let $M$ be a Dedekind complete model of $T$. Let $\phi(\mathbf{x}, \mathbf{y})$ be an $L$-formula where $l(\mathbf{y}) = k$. Let $\mathbf{X} = \{X \subset M^k$: for some $\mathbf{a}$ in an elementary extension $N$ of $M, X = \phi (\mathbf{a,y}^N \cap M^k\}$. Then there is a formula $\psi(\mathbf{y}, \mathbf{z})$ of $L$ such that $\mathbf{X} = \{\psi (\mathbf{y, b})^M: \mathbf{b}$ in $M\}$.