> [!theorem]
>
> Let $(\Omega, \cf, \bp, T)$ be an [[Ergodic Measure System|ergodic system]] and $E \in \cf$, then there exists $E_0 \subset E$ such that
> 1. $\mu(E_0) = \mu(E)$.
> 2. For any $x \in E_0$, there exists $n \in \nat$ such that $T^nx \in E_0$.
>
> *Proof*. Let
> $
> W = \bracs{x \in E: T^nx \not\in E \forall n \in \nat}
> $
> then $W \cap T^{-n}(W) = \emptyset$ for all $n \in \nat$,
> $
> \bp\bracs{\bigsqcup_{n \in \nat}T^{-n}(W)} = \sum_{n \in \nat}\bp\bracs{T^{-n}(W)} = \sum_{n \in \nat}\bp\bracs{W} < \infty
> $
> so $\bp\bracs{W} = 0$, and $E_0 = E \setminus \bigcup_{n \ge 0}T^{-n}(W)$ is the desired set.