Add simple lemmas on filters

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}