Let $P = (X, {\preceq})$ be an D1707: Ordered set.
A D11: Set $D \subseteq X$ is a Dedekind cut in $P$ if and only if

(1)	\begin{equation} \emptyset \neq C \neq X \end{equation}
(2)	\begin{equation} \forall \, x \in X : \forall \, c \in C \left( (x, c) \in {\preceq} \quad \implies \quad x \in c \right) \end{equation}
(3)	\begin{equation} \forall \, c \in C : \exists \, c' \in C : (c, c') \in {\preceq} \end{equation}