Since we can write \begin{equation} \bigcap_{n = 0}^{\infty} E_n = E_0 \cap \left( \bigcap_{n = 1}^{\infty} E_n \right) = E_0 \cap F \end{equation} with $F : = \bigcap_{n = 1}^{\infty} E_n$, then this result is a consequence of R4331: Probability of binary intersection with an almost sure event. $\square$