From a5deeef9c3214f0f2ccd90789f5344a88544d65b Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 25 May 2024 01:21:17 +0200
Subject: Prove `emptyset_open` to replace structure axiom

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

(limited to 'library/set.tex')

diff --git a/library/set.tex b/library/set.tex
index e7e062f..fcd2642 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -131,8 +131,7 @@ which applies it to goals of the form “$A = B$” and  “$A \neq B$”.
     If $x$ and $y$ are empty, then $x = y$.
 \end{proposition}
 
-\begin{proposition}%
-\label{emptyset_subseteq}
+\begin{proposition}\label{emptyset_subseteq}
     For all $a$ we have $\emptyset \subseteq a$.
     % LATER $\emptyset$ is a subset of every set.
 \end{proposition}
@@ -266,8 +265,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     There exists $B\in C$ such that $A\in B$.
 \end{proof}
 
-\begin{proposition}%
-\label{unions_emptyset}
+\begin{proposition}\label{unions_emptyset}
     $\unions{\emptyset} = \emptyset$.
 \end{proposition}
 
-- 
cgit v1.2.3