From 3845ab9020b3eb591ef999827503b483eb735bd7 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 21 May 2024 16:52:01 +0200
Subject: Add simple lemmas on filters

---
 library/set.tex | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'library/set.tex')

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}
-- 
cgit v1.2.3