Change order of two lemmas in algebra

algebra.tex

@@ -8885,27 +8885,8 @@ \section{Flat modules and flat ring maps}
 Immediate from Lemma \ref{lemma-ff-rings}.
 \end{proof}
 
-\begin{lemma}
-\label{lemma-flat-going-down}
-Let $R \to S$ be flat. Let $\mathfrak p \subset \mathfrak p'$
-be primes of $R$. Let $\mathfrak q' \subset S$ be a prime of $S$
-mapping to $\mathfrak p'$. Then there exists a prime
-$\mathfrak q \subset \mathfrak q'$ mapping to $\mathfrak p$.
-\end{lemma}
-
-\begin{proof}
-Namely, consider the flat local ring map
-$R_{\mathfrak p'} \to S_{\mathfrak q'}$.
-By Lemma \ref{lemma-local-flat-ff} this is faithfully
-flat. By Lemma \ref{lemma-ff-rings} there is a prime mapping to
-$\mathfrak p R_{\mathfrak p'}$. The inverse image of this
-prime in $S$ does the job.
-\end{proof}
-
 \noindent
-The property of $R \to S$ described in the lemma is called the
-``going down property''. See Definition \ref{definition-going-up-down}.
-We finish with some remarks on flatness and localization.
+Flatness meshes well with localization.
 
 \begin{lemma}
 \label{lemma-flat-localization}
@@ -8976,6 +8957,27 @@ \section{Flat modules and flat ring maps}
 way from the last statement (proofs omitted).
 \end{proof}
 
+\begin{lemma}
+\label{lemma-flat-going-down}
+Let $R \to S$ be flat. Let $\mathfrak p \subset \mathfrak p'$
+be primes of $R$. Let $\mathfrak q' \subset S$ be a prime of $S$
+mapping to $\mathfrak p'$. Then there exists a prime
+$\mathfrak q \subset \mathfrak q'$ mapping to $\mathfrak p$.
+\end{lemma}
+
+\begin{proof}
+By Lemma \ref{lemma-flat-localization} the local ring map
+$R_{\mathfrak p'} \to S_{\mathfrak q'}$ is flat.
+By Lemma \ref{lemma-local-flat-ff} this local ring map is faithfully
+flat. By Lemma \ref{lemma-ff-rings} there is a prime mapping to
+$\mathfrak p R_{\mathfrak p'}$. The inverse image of this
+prime in $S$ does the job.
+\end{proof}
+
+\noindent
+The property of $R \to S$ described in the lemma is called the
+``going down property''. See Definition \ref{definition-going-up-down}.
+
 \begin{lemma}
 \label{lemma-colimit-faithfully-flat}
 Let $R$ be a ring. Let $\{S_i, \varphi_{ii'}\}$ be a directed system of