\begin{definition}[Definition:Dedekind Completion]
Let $S$ be an ordered set.
A '''Dedekind completion of $S$''' is a Dedekind complete ordered set $\tilde S$ together with an order embedding $\phi: S \to \tilde S$, subject to:
:For all Dedekind complete ordered sets $X$, and for all order embeddings $f: S \to X$, there exists a unique order embedding $\tilde f: \tilde S \to X$ such that:
::$\tilde f \circ \phi = f$
\end{definition}