\begin{frame}
  \small

  \begin{lemma}
  \smallskip
  ARS $\AA = \langle A, \to_1 \rangle$ is confluent if
  \begin{itemize}
    \item ${\to_1} \:\subseteq\: \mathrel{\alert{\to_2}} \:\subseteq\: {\to_1^*}$
  \end{itemize}
  for a confluent relation \alert{$\to_2$} on $A$.
  \smallskip
  \end{lemma}
  \medskip
  
  \begin{proof}<2->
  \onslide<3->
  Assume $\to_2$ is confluent, that is, ${\FromBP{2}{*} \cdot \to_2^*} \;\subseteq\; {\to_2^* \cdot \FromBP{2}{*}}$.
  \begin{itemize}
    \item<4-> From ${\to_1} \;\subseteq\; {\to_2}$ follows ${\to_1^*} \;\subseteq\; {\to_2^*}$.
    \item<5-> Moreover ${\to_2^*} \;\subseteq\; {\to_1^*}$ since ${\to_1^*}$ is transitive and contains ${\to_2}$.
  \end{itemize}
  \onslide<6->
  Hence ${\to_1^*} \;=\; {\to_2^*}$.\\
  \onslide<7->
  $\implies \quad {\FromBP{1}{*} \cdot \to_1^*} \;\subseteq\; {\to_1^* \cdot \FromBP{1}{*}}$
  \end{proof}
\end{frame}