Result
R981: Countably infinite measurable cover has measurable subcover shows that there exists measurable, disjoint sets $F_0, F_1, F_2, \ldots \in \mathcal{F}$ such that $F_n \subseteq E_n$ for every $n \in \mathbb{N}$ and that $\bigcup_{n \in \mathbb{N}} E_n = \bigcup_{n \in \mathbb{N}} F_n$. As a consequence, result
R975: Isotonicity of unsigned basic measure shows that $\mu(F_n) \subseteq \mu(E_n)$ for every $n \in \mathbb{N}$. Thus, applying disjoint additivity of $\mu$ and result
R3651: Isotonicity of unsigned basic series, we have
\begin{equation}
\mu \left( \bigcup_{n \in \mathbb{N}} E_n \right)
= \mu \left( \bigcup_{n \in \mathbb{N}} F_n \right)
= \sum_{n \in \mathbb{N}} \mu(F_n)
\leq \sum_{n \in \mathbb{N}} \mu(E_n)
\end{equation}
$\square$
