From 9762647b0ef8556301b991a4352a6aa9bafc0913 Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 23 May 2026 21:24:52 +0200
Subject: [PATCH 1/5] theorem

---
 theorems/T000895.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 theorems/T000895.md

diff --git a/theorems/T000895.md b/theorems/T000895.md
new file mode 100644
index 000000000..fa1929810
--- /dev/null
+++ b/theorems/T000895.md
@@ -0,0 +1,16 @@
+---
+uid: T000894
+if:
+  and:
+  - P000039 : false
+  - P000078: false
+  - P000219: false
+then:
+  P000139: false
+---
+
+Since $X$ is not {P39}, there is a nonempty open set $U$ which is not dense. Let $x_0 \in U$ and $x_1 \in X\setminus \overline{U}$.
+
+Since $X$ is infinite, we either have $|U \cup \{x_1\}| = |X|$ or $|(X \setminus U) \cup \{x_0\}| = |X|$.
+
+Both $U \cup \{x_1\}$ and $(X \setminus U) \cup \{x_0\}$ contain an isolated point, thus the assertion follows by {P219}.

From f549feb9e05eb5449114e39f2f569aa8bb316a1a Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 23 May 2026 21:25:09 +0200
Subject: [PATCH 2/5] fix

---
 theorems/T000895.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theorems/T000895.md b/theorems/T000895.md
index fa1929810..34122832a 100644
--- a/theorems/T000895.md
+++ b/theorems/T000895.md
@@ -4,9 +4,9 @@ if:
   and:
   - P000039 : false
   - P000078: false
-  - P000219: false
+  - P000219: true
 then:
-  P000139: false
+  P000139: true
 ---
 
 Since $X$ is not {P39}, there is a nonempty open set $U$ which is not dense. Let $x_0 \in U$ and $x_1 \in X\setminus \overline{U}$.

From 25b26e05692706a9968d4082dd04c9b9ecf3616f Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 23 May 2026 21:38:35 +0200
Subject: [PATCH 3/5] wrong uid

---
 theorems/T000895.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000895.md b/theorems/T000895.md
index 34122832a..45edfd685 100644
--- a/theorems/T000895.md
+++ b/theorems/T000895.md
@@ -1,5 +1,5 @@
 ---
-uid: T000894
+uid: T000895
 if:
   and:
   - P000039 : false

From d83aa93d5d924309a925582f889e753c1e7bc49e Mon Sep 17 00:00:00 2001
From: Batixx <s59fpern@uni-bonn.de>
Date: Sat, 23 May 2026 21:39:58 +0200
Subject: [PATCH 4/5] move uid

---
 theorems/{T000895.md => T000898.md} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename theorems/{T000895.md => T000898.md} (97%)

diff --git a/theorems/T000895.md b/theorems/T000898.md
similarity index 97%
rename from theorems/T000895.md
rename to theorems/T000898.md
index 45edfd685..a9625dc0a 100644
--- a/theorems/T000895.md
+++ b/theorems/T000898.md
@@ -1,5 +1,5 @@
 ---
-uid: T000895
+uid: T000898
 if:
   and:
   - P000039 : false

From ecdd0b38f4fbcb658870cf2a11016a0230be8097 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sun, 24 May 2026 07:58:53 +0200
Subject: [PATCH 5/5] Update theorems/T000898.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000898.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000898.md b/theorems/T000898.md
index a9625dc0a..a6740854f 100644
--- a/theorems/T000898.md
+++ b/theorems/T000898.md
@@ -2,9 +2,9 @@
 uid: T000898
 if:
   and:
+  - P000219: true
   - P000039 : false
   - P000078: false
-  - P000219: true
 then:
   P000139: true
 ---