Pow closed under binary intersection

1 files changed, 5 insertions, 8 deletions

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$.