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}
▶ | D4978: Basic rational closed unit interval |