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.

1 files changed, 5 insertions, 1 deletions

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