Fix statement and proof of proposition in derived

Thanks to  Elías Guisado
https://stacks.math.columbia.edu/tag/05SE#comment-8386

derived.tex

@@ -4879,10 +4879,12 @@ \section{Derived functors in general}
 of triangulated categories.
 \item Elements of $S$ with either source or target
 in $\mathcal{E}$ are morphisms of $\mathcal{E}$.
-\item The functor $S_\mathcal{E}^{-1}\mathcal{E} \to S^{-1}\mathcal{D}$
-is a fully faithful exact functor of triangulated categories.
 \item Any element of $S_\mathcal{E} = \text{Arrows}(\mathcal{E}) \cap S$
 is mapped to an isomorphism by $RF$.
+\item The set $S_\mathcal{E}$ is a saturated multiplicative system in
+$\mathcal{E}$ compatible with the triangulated structure.
+\item The functor $S_\mathcal{E}^{-1}\mathcal{E} \to S^{-1}\mathcal{D}$
+is a fully faithful exact functor of triangulated categories.
 \item We obtain an exact functor
 $$
 RF : S_\mathcal{E}^{-1}\mathcal{E} \longrightarrow \mathcal{D}'.
@@ -4896,24 +4898,26 @@ \section{Derived functors in general}
 \begin{proof}
 Since $S$ is saturated it contains all isomorphisms (see remark
 following Categories, Definition
-\ref{categories-definition-saturated-multiplicative-system}). Hence
-(1) follows from Lemmas \ref{lemma-derived-inverts},
-\ref{lemma-2-out-of-3-defined}, and
-\ref{lemma-derived-shift}. We get (2) from
-Lemmas \ref{lemma-derived-functor}, \ref{lemma-derived-shift}, and
-\ref{lemma-2-out-of-3-defined}. We get (3) from
-Lemma \ref{lemma-derived-inverts}. The fully faithfulness in (4) follows
-from (3) and the definitions. The fact that
-$S_\mathcal{E}^{-1}\mathcal{E} \to S^{-1}\mathcal{D}$ is exact
-follows from the fact that a triangle in $S_\mathcal{E}^{-1}\mathcal{E}$
-is distinguished if and only if it is isomorphic to the image of a
+\ref{categories-definition-saturated-multiplicative-system}).
+Hence (1) follows from Lemmas \ref{lemma-derived-inverts},
+\ref{lemma-2-out-of-3-defined}, and \ref{lemma-derived-shift}.
+We get (2) from Lemmas \ref{lemma-derived-functor}, \ref{lemma-derived-shift},
+and \ref{lemma-2-out-of-3-defined}.
+We get (3) from Lemma \ref{lemma-derived-inverts}.
+Part (4) follows from Lemma \ref{lemma-derived-inverts}.
+Part (5) follows from the definitions and part (3).
+The fully faithfulness in (6) follows from (3) and
+the definitions. The fact that
+$S_\mathcal{E}^{-1}\mathcal{E} \to S^{-1}\mathcal{D}$
+is exact follows from the fact that a triangle in
+$S_\mathcal{E}^{-1}\mathcal{E}$ is distinguished
+if and only if it is isomorphic to the image of a
 distinguished triangle in $\mathcal{E}$, see proof of
 Proposition \ref{proposition-construct-localization}.
-Part (5) follows from Lemma \ref{lemma-derived-inverts}.
 The factorization of $RF : \mathcal{E} \to \mathcal{D}'$
 through an exact functor $S_\mathcal{E}^{-1}\mathcal{E} \to \mathcal{D}'$
 follows from Lemma \ref{lemma-universal-property-localization}.
-Part (7) follows from Lemma \ref{lemma-direct-sum-defined}.
+Finally, part (8) follows from Lemma \ref{lemma-direct-sum-defined}.
 \end{proof}
 
 \noindent