From ab4ddd9d49349ddb781514b6b0e9060db5b66a22 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 12 Jun 2024 13:47:38 +0200
Subject: Prove Bug "Ex falso quodlibet"

The generated ATP Tasks are done in few secounds, if they are send manually to Vampire. But if its done in Naproche all together it won't work.
---
 library/topology/topological-space.tex | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index 2590287..dd236bb 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -233,7 +233,11 @@
 \end{proposition}
 \begin{proof}
     \begin{byCase}
-        \caseOf{$F$ is empty.} Trivial.
+        \caseOf{$F$ is empty.} 
+        For all $X$ we have $X \notin F$.
+        If $X \in F$ and $A \in X$ then $A \in F$.
+        %There exist $X \in F$.
+        Contradiction by assumption.
         \caseOf{$F$ is inhabited.}
         There exist $X \in F$ such that $X \subseteq \unions{F}$.
         $A \subseteq X \subseteq \unions{F}$.
-- 
cgit v1.2.3