1 files changed, 13 insertions, 5 deletions
diff --git a/library/topology/disconnection.tex b/library/topology/disconnection.tex
index e3730f3..90c635d 100644
--- a/library/topology/disconnection.tex
+++ b/library/topology/disconnection.tex
@@ -23,10 +23,14 @@
     Then there exists a disconnection of $X$.
 \end{proposition}
 \begin{proof}
-    Take $U, V\in\opens[X]$ such that $\carrier[X]$ is partitioned by $U$ and $V$
+    Take $U,V$ such that $U,V\in\opens[X]$ and
+        $\carrier[X]$ is partitioned by $U$ and $V$
         by \cref{disconnected}.
-    Then $(U, V)$ is a bipartition of $\carrier[X]$.
-    Thus $(U, V)$ is a disconnection of $X$ by \cref{disconnections,times_proj_elim,times_tuple_intro}.
+    $(U,V)$ is a bipartition of $\carrier[X]$ by \cref{bipartition_intro}.
+    $\fst{(U,V)}=U$ by \cref{fst_eq}.
+    $\snd{(U,V)}=V$ by \cref{snd_eq}.
+    $(U,V)\in\disconnections{X}$ by \cref{disconnections}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{disconnected_from_disconnection}
@@ -35,8 +39,12 @@
     Then $X$ is disconnected.
 \end{proposition}
 \begin{proof}
-    $\fst{D}, \snd{D}\in\opens[X]$.
-    $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$.
+    $D\in\disconnections{X}$ by assumption.
+    $D\in\bipartitions{\carrier[X]}$ by \cref{disconnections}.
+    $\fst{D},\snd{D}\in\opens[X]$ by \cref{disconnections}.
+    $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$
+        by \cref{bipartitions_of_a_set}.
+    Follows by \cref{disconnected}.
 \end{proof}
 
 \begin{abbreviation}\label{connected}