summaryrefslogtreecommitdiff
path: root/library/set.tex
diff options
context:
space:
mode:
Diffstat (limited to 'library/set.tex')
-rw-r--r--library/set.tex10
1 files changed, 6 insertions, 4 deletions
diff --git a/library/set.tex b/library/set.tex
index 33e5af4..e7e062f 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -553,13 +553,15 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
Follows by set extensionality.
\end{proof}
-\begin{proposition}%
-\label{inter_subseteq}
+\begin{proposition}\label{inter_subseteq_left}
$A\inter B\subseteq A$.
\end{proposition}
-\begin{proposition}%
-\label{inter_emptyset}
+\begin{proposition}\label{inter_subseteq_right}
+ $A\inter B\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{inter_emptyset}
$A\inter\emptyset = \emptyset$.
\end{proposition}
\begin{proof}