summaryrefslogtreecommitdiff
path: root/library/ordinal.tex
diff options
context:
space:
mode:
Diffstat (limited to 'library/ordinal.tex')
-rw-r--r--library/ordinal.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/ordinal.tex b/library/ordinal.tex
index 6f924c1..c092fa8 100644
--- a/library/ordinal.tex
+++ b/library/ordinal.tex
@@ -559,7 +559,7 @@ Then $\alpha\subseteq\beta$.
\end{lemma}
\begin{proof}
Suppose not.
- Then $\emptyset\precedes \emptyset$ by \cref{notin_emptyset,limit_ordinal}.
+ Then $\emptyset\precedes \emptyset$ by \cref{emptyset,limit_ordinal}.
Thus $\emptyset\in \emptyset$.
Contradiction.
\end{proof}
@@ -636,4 +636,4 @@ Then $\alpha\subseteq\beta$.
% $\emptyset\precedes \naturals$.
% If $n\in \naturals$, then $\suc{n}\in\naturals$.
%\end{proof}
-% \ No newline at end of file
+%