1 files changed, 38 insertions, 5 deletions
diff --git a/library/order/quasiorder.tex b/library/order/quasiorder.tex
index ab325e7..3ccb46e 100644
--- a/library/order/quasiorder.tex
+++ b/library/order/quasiorder.tex
@@ -37,15 +37,48 @@
     Then $a\mathrel{\lt[X]} d$.
 \end{lemma}
 \begin{proof}
-    $\lt[X]$ is transitive.
-    Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}.
-    Hence $a\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}.
+    $\lt[X]$ is transitive by \cref{quasiorder_tran}.
+    Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \cref{transitive}.
+    Hence $a\mathrel{\lt[X]} d$ by \cref{transitive}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{subseteqrel_is_quasiorder}
     $\subseteqrel{A}$ is a quasiorder on $A$.
 \end{proposition}
 \begin{proof}
-    $\subseteqrel{A}$ is reflexive on $A$.
-    $\subseteqrel{A}$ is transitive.
+    Show for all $w\in\subseteqrel{A}$ we have $w\in A\times A$.
+    \begin{subproof}
+        Fix $w$.
+        Assume $w\in\subseteqrel{A}$.
+        Take $a,b$ such that $w=(a,b)$ and $a,b\in A$
+            by \cref{subseteqrel,pair_eq_iff}.
+        Follows by \cref{times_tuple_intro}.
+    \end{subproof}
+    Thus $\subseteqrel{A}$ is a binary relation on $A$
+        by \cref{subseteq}.
+    $\subseteqrel{A}$ is reflexive on $A$
+        by \cref{reflexive_on,subseteqrel,subseteq}.
+    Show for all $a,b,c$ such that
+        $a\mathrel{\subseteqrel{A}}b$ and
+        $b\mathrel{\subseteqrel{A}}c$
+        we have $a\mathrel{\subseteqrel{A}}c$.
+    \begin{subproof}
+        Fix $a,b,c$.
+        Assume $a\mathrel{\subseteqrel{A}}b$ and
+            $b\mathrel{\subseteqrel{A}}c$.
+        Take $x,y$ such that $(a,b)=(x,y)$ and
+            $x,y\in A$ and $x\subseteq y$ by \cref{subseteqrel}.
+        Then $a=x$ and $b=y$ by \cref{pair_eq_iff}.
+        Thus $a\subseteq b$ and $a\in A$ by assumption.
+        Take $u,v$ such that $(b,c)=(u,v)$ and
+            $u,v\in A$ and $u\subseteq v$ by \cref{subseteqrel}.
+        Then $b=u$ and $c=v$ by \cref{pair_eq_iff}.
+        Thus $b\subseteq c$ and $c\in A$ by assumption.
+        Thus $a\subseteq c$ by \cref{subseteq_transitive}.
+        Follows by \cref{subseteqrel}.
+    \end{subproof}
+    Thus $\subseteqrel{A}$ is transitive
+        by \cref{transitive}.
+    Follows by assumption.
 \end{proof}