\begin{definition}[Definition:Order Completion]
Let $\struct {S, \preceq_S}$ be an ordered set.
An ordered set $\struct {T, \preceq_T}$ is an '''order completion of $S$''' {{iff}}:
:$(1):\quad S \subseteq T$
:$(2):\quad {\preceq_T \restriction_S} = {\preceq_S}$, where $\restriction$ denotes restriction
:$(3):\quad \struct {T, \preceq_T}$ is a complete ordered set
:$(4):\quad$ For all ordered sets $\struct {T', \preceq_{T'} }$ satisfying $(1), (2)$ and $(3)$, there is a unique order-preserving injection $\phi: T' \to T$
\end{definition}