%
\label{thm:congruence-axioms}
The congruence relation $\cong$
(Definition~\ref{def:congruence})
satisfies the Tarski congruence axioms:
\begin{enumerate}
    \item[\textup{(C1)}] Reflexivity:
          $AB \cong BA$.
    \item[\textup{(C2)}] Identity of congruence:
          $AB \cong CC \implies A = B$.
    \item[\textup{(C3)}] Transitivity:
          $AB \cong CD,\; CD \cong EF \implies AB \cong EF$.
    \item[\textup{(C4)}] Segment construction:
          given $A$, $B$, $C$, $D$ with $C \neq D$,
          there exists~$E$ with $B(C,D,E)$
          and $DE \cong AB$.
    \item[\textup{(C5)}] Five-segment:
          $A \neq B$,
          $B(A,B,C)$, $B(A',B',C')$,
          $AB \cong A'B'$, $BC \cong B'C'$,
          $AD \cong A'D'$, $BD \cong B'D'$
          imply $CD \cong C'D'$.
    \item[\textup{(C6)}] Inner transitivity:
          $B(A,B,D)$, $B(A,C,E)$,
          $AB \cong AC$, $BD \cong CE$
          imply $AD \cong AE$.
\end{enumerate}

Propositions~\ref{prop:ch19-c1-c3},
\ref{prop:ch19-c4},
\ref{prop:ch19-c5},
and~\ref{prop:ch19-c6}
verify each axiom individually.