summaryrefslogtreecommitdiff
path: root/library/set.tex
diff options
context:
space:
mode:
Diffstat (limited to 'library/set.tex')
-rw-r--r--library/set.tex6
1 files changed, 2 insertions, 4 deletions
diff --git a/library/set.tex b/library/set.tex
index e7e062f..fcd2642 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -131,8 +131,7 @@ which applies it to goals of the form “$A = B$” and “$A \neq B$”.
If $x$ and $y$ are empty, then $x = y$.
\end{proposition}
-\begin{proposition}%
-\label{emptyset_subseteq}
+\begin{proposition}\label{emptyset_subseteq}
For all $a$ we have $\emptyset \subseteq a$.
% LATER $\emptyset$ is a subset of every set.
\end{proposition}
@@ -266,8 +265,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
There exists $B\in C$ such that $A\in B$.
\end{proof}
-\begin{proposition}%
-\label{unions_emptyset}
+\begin{proposition}\label{unions_emptyset}
$\unions{\emptyset} = \emptyset$.
\end{proposition}