By
R2556: Probability calculus expression for probability conditioned on event of nonzero probability, we have
\begin{equation}
1
= \mathbb{P}(F \mid E)
= \frac{\mathbb{P}(E \cap F)}{\mathbb{P}(E)}
= \mathbb{P}(E \cap F)
\end{equation}
Whence, from
R4331: Probability of binary intersection with an almost sure event, we have
\begin{equation}
1
= \mathbb{P}(E \cap F)
= \mathbb{P}(F)
\end{equation}
$\square$
