
Lemma
Proof.
Since A is nonempty, we take an arbitrary infinite word \(w \in L (A)\). Suppose \(w = a_1 a_2 \cdots\).
From the acceptance condition of Buchi automaton, we know there must be at least one final state \(q_f \in F\) that occurs in \(w\) infinitely often. Assume at position i, after reading prefix \(a_1 \cdots a_i\), \(q_f\) is reached for the first time, and at position j it is reached for the second time.
Then consider the infinite word \(w' = a_1 \cdots a_i (a_{i + 1} \cdots a_j)^{\omega}\). Obviously \(w' \in L (A)\) and it satisfies the condition.