diff options
Diffstat (limited to 'library/set.tex')
| -rw-r--r-- | library/set.tex | 6 |
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} |
