\begin{definition}[Definition:Real Interval/Length]
Let:
:$\closedint a b$
or
:$\hointr a b$
or
:$\hointl a b$
or
:$\openint a b$
be a real interval.
The difference $b - a$ between the endpoints is called the '''length''' of the interval.
\end{definition}