From 719bb860942fc1134ad4a4ae55db2713cd100f1a Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 28 May 2024 17:09:06 +0200
Subject: Pow closed under binary intersection

---
 library/set.tex | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'library/set.tex')

diff --git a/library/set.tex b/library/set.tex
index fcd2642..2fd18ea 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -551,14 +551,6 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}\label{inter_subseteq_left}
-    $A\inter B\subseteq A$.
-\end{proposition}
-
-\begin{proposition}\label{inter_subseteq_right}
-    $A\inter B\subseteq B$.
-\end{proposition}
-
 \begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
@@ -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$.
-- 
cgit v1.2.3