Merge pull request #2 from adelon/main

changes from main needs to be included

1 files changed, 8 insertions, 11 deletions

diff --git a/library/set.tex b/library/set.tex
index 33e5af4..2fd18ea 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}
 
@@ -553,13 +551,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}%
-\label{inter_subseteq}
-    $A\inter B\subseteq A$.
-\end{proposition}
-
-\begin{proposition}%
-\label{inter_emptyset}
+\begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
 \begin{proof}
@@ -620,6 +612,11 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
+\begin{proposition}\label{inter_subseteq}
+    Suppose $A,B\subseteq C$.
+    Then $A\inter B\subseteq C$.
+\end{proposition}
+
 \begin{abbreviation}\label{closedunderinter}
     $T$ is closed under binary intersections
     iff for every $U,V\in T$ we have $U\inter V\in T$.