Let $P = (\mathbb{R}, {\leq})$ be the D1102: Ordered set of real numbers.
The closed real unit interval is the D11: Set \begin{equation} [0, 1] : = \{ x \in \mathbb{R} : 0 \leq x \leq 1 \} \end{equation}