David Williams: "Probability with martingales" Kolmogorov 3-series theorem proof I don't understand the form of the Borel-Cantelli lemma used in the proof of the Kolmogorov 3-series theorem:

However I see the Borel-Cantelli lemma as being:

So I would say that the BC lemma states that $P(X_n \ne X_n^K$ ,infinitely often) = 0, so that $P(X_n = X_n^K$, infinitely often) =1 , rather than $P(X_n = X_n^K$, eventually) =1 ?
 A: We have that
$$(X_n\neq X_n^K,\text{ i.o})=\left\{\omega\::\: X_n(\omega)\neq X_n^K(\omega),\text{ i.o}\right)$$
$$=\left\{\omega\::\: \forall n\in\mathbb{N},\:\exists m>n\text{ with } X_m(\omega)\neq X_n^K(\omega)\right\}.$$
The negation of $$\forall n\in\mathbb{N},\:\exists m>n\text{ with } X_m(\omega)\neq X_n^K(\omega)$$ is:
$$\exists n\in\mathbb{N}\text{ such that }\forall m>n \text{ it holds }X_m(\omega)=X_n^K.$$
Therefore $\{\omega\::\: X_n(\omega)\neq X_n^K(\omega),\text{ i.o}\}^c=\{\omega\:;\:X_n(\omega)= X_n^K(\omega),\text{ eventually}\}$.
Then if $P(X_n\neq X_n^K,\text{ i.o})=0$, then $P(X_n= X_n^K,\text{ eventually})=1$.
A: Recall the limsup and liminf definitions of sequences of sets. By BC1, we have
\begin{align*}
0 &= P(\limsup \{X_n \neq X_n^K\}) \\
&= P(\cap_m \cup_{n > m} \{X_n \neq X_n^K\}) \\
&= 1 - P(\cup_m \cap_{n > m} \{X_n = X_n^K\}) \\
\Rightarrow 1 &= P(\liminf \{X_n = X_n^K\})
\end{align*}
where limsup corresponds to infinitely often and liminf corresponds to all but finitely many.
