From 9d34eebafc87e6bce476ccc487a88b440315089b Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 8 Jul 2025 21:46:54 +0200
Subject: Optimize proof

---
 library/topology/topological-space.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/topology/topological-space.tex')

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 6ddf721..5209a13 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -291,7 +291,7 @@
         \end{subproof}
         $\closures{A}{X}$ is inhabited.
         For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$.
-        Therefore $A \subseteq \inters{\closures{A}{X}}$.
+        Therefore $A \subseteq \inters{\closures{A}{X}}$ by \cref{subseteq_inters_iff}.
     \end{byCase}
 \end{proof}
 
-- 
cgit v1.2.3