\begin{frame}
  \frametitle{Transitive Frames: $\some\some p \to \some p$}

  \begin{goal}{Theorem}
    \begin{malign}
      \F \models \some\some p \to \some p \quad\iff\quad \text{the frame $\F$ is transitive}
    \end{malign}
  \end{goal}
  \pause

  \begin{block}{Proof ($\Leftarrow$)}
  \begin{itemize}
    \pause
    \item Let $\F = (W,R)$ be a frame where $R$ is transitive.
    \pause
    \item Let $L$ be an arbitrary labelling, and $x$ a world in $W$.
    \pause
    \item We show $x \fc \some\some p \to \some p$.\\
    \pause
          That is, if $x\fc \some\some p$, then also $x\fc  \some p$.
    \pause 
    \item Thus assume that $x \fc \some\some p$.
    \pause
    \item Then there exists $y\in W$ with $R(x,y)$ and $y \fc \some p$.
    \pause
    \item Then there exists $z \in W$ with $R(y,z)$ and $z \fc p$.
    \pause
    \item Because of transitivity of $R$ we have $R(x,z)$.
    \pause
    \item Hence $x \fc \some p$.
  \end{itemize}
  \end{block}
  \vspace{10cm}
\end{frame}