\newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
\newcommand{\qed}{\square}
-\newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
+\newcommand{\proofstarts}{{\it Proof:}}
+\newcommand{\proof}[1]{\proofstarts #1 $\qed$}
\newcommand{\gathbegin}{\begin{gather} \tag*{}}
\newcommand{\gathnext}{\\ \tag*{}}
\gathnext
R \le C
\end{gather}
-No Replay is preserved. {\it Proof:}
+No Replay is preserved. \proofstarts
\subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
\subsection{Desired Contents}
\[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
-{\it Proof.}
+\proofstarts
\subsubsection{For $D = C$:}