From 350d3b762303250f79d4644152f734aed100bc37 Mon Sep 17 00:00:00 2001
From: JSMassmann <sylvie@83c.nl>
Date: Thu, 25 Jun 2026 18:14:30 +0100
Subject: [PATCH 01/14] Add the three theorems in the branch name; placeholder
 proofs for two.

---
 theorems/T000908.md | 11 +++++++++++
 theorems/T000909.md | 12 ++++++++++++
 theorems/T000910.md | 11 +++++++++++
 3 files changed, 34 insertions(+)
 create mode 100644 theorems/T000908.md
 create mode 100644 theorems/T000909.md
 create mode 100644 theorems/T000910.md

diff --git a/theorems/T000908.md b/theorems/T000908.md
new file mode 100644
index 000000000..b0ed0c325
--- /dev/null
+++ b/theorems/T000908.md
@@ -0,0 +1,11 @@
+---
+uid: T000908
+if:
+  and:
+  - P000203: true
+  - P000026: true
+then:
+  P000057: true
+---
+
+Letting $x$ be the only point which is not isolated, and $Y$ be a countable dense set, for every $y \neq x$, $\{y\}$ is nonempty and open, so $\{y\} \cap Y \neq \emptyset$, so $y \in Y$. Therefore $X \setminus \{x\} \subseteq Y$, so $X \setminus \{x\}$ is countable, so $X$ is countable.
diff --git a/theorems/T000909.md b/theorems/T000909.md
new file mode 100644
index 000000000..3d44136ed
--- /dev/null
+++ b/theorems/T000909.md
@@ -0,0 +1,12 @@
+---
+uid: T000909
+if:
+  and:
+  - P000002: true
+  - P000174: true
+  - P000244: true
+then:
+  P000028: true
+---
+
+Placeholder!!!!!
diff --git a/theorems/T000910.md b/theorems/T000910.md
new file mode 100644
index 000000000..1628a3753
--- /dev/null
+++ b/theorems/T000910.md
@@ -0,0 +1,11 @@
+---
+uid: T000910
+if:
+  and:
+  - P000222: true
+  - P000244: true
+then:
+  P000057: true
+---
+
+Placeholder!!!!!

From 2c39627fcc1a7a22cf5fd7fbf8dd5e62d1ec8c19 Mon Sep 17 00:00:00 2001
From: JSMassmann <sylvie@83c.nl>
Date: Thu, 25 Jun 2026 19:14:37 +0100
Subject: [PATCH 02/14] Add actual proof for T910

---
 theorems/T000910.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theorems/T000910.md b/theorems/T000910.md
index 1628a3753..6f0828ff7 100644
--- a/theorems/T000910.md
+++ b/theorems/T000910.md
@@ -8,4 +8,6 @@ then:
   P000057: true
 ---
 
-Placeholder!!!!!
+Let $x \in X$ and $\mathcal{V}$ be a countable local $\pi$-base around $x$. Set $W = \bigcup\{X \setminus V: V \in \mathcal{V}\}$. For any $y \neq x$, $X \setminus \{y\}$ is a neighbourhood of $x$ and so there is $V \in \mathcal{V}$ with $V \subseteq X \setminus \{y\}$. Therefore $y \in X \setminus V \subseteq W$ so, since $y$ was arbitrary, $X \setminus \{x\} \subseteq W$. But $W$ is a countable union of finite sets, so $W$ is countable, so $X$ is countable.
+
+Observe that the above argument only requires some point to have a countable local $\pi$-base, not every point.

From d65d37c5d247123bf8ddd22b9bf7eb76dc96b3c0 Mon Sep 17 00:00:00 2001
From: JSMassmann <sylvie@83c.nl>
Date: Thu, 25 Jun 2026 20:22:43 +0100
Subject: [PATCH 03/14] Add actual proof for T909

---
 theorems/T000909.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theorems/T000909.md b/theorems/T000909.md
index 3d44136ed..1ca042a7f 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -9,4 +9,6 @@ then:
   P000028: true
 ---
 
-Placeholder!!!!!
+Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$). Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$; by $T_1$, we can choose some $U_A \in \mathcal{U}$ with $U_A \subseteq A \setminus \{a\}$.
+
+Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$, hence a local base for $x$. But if $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.

From edb597cf2630727c1be43dc3f4da227722314f94 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Fri, 26 Jun 2026 08:41:33 +0100
Subject: [PATCH 04/14] Update theorems/T000909.md

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

diff --git a/theorems/T000909.md b/theorems/T000909.md
index 1ca042a7f..ff7b17a11 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -2,9 +2,9 @@
 uid: T000909
 if:
   and:
-  - P000002: true
   - P000174: true
   - P000244: true
+  - P000002: true
 then:
   P000028: true
 ---

From 7c5d0198d177b5e3c8614bbe82e67bc4d9921f70 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Fri, 26 Jun 2026 08:45:14 +0100
Subject: [PATCH 05/14] Update theorems/T000909.md

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

diff --git a/theorems/T000909.md b/theorems/T000909.md
index ff7b17a11..f399faca3 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -11,4 +11,5 @@ then:
 
 Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$). Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$; by $T_1$, we can choose some $U_A \in \mathcal{U}$ with $U_A \subseteq A \setminus \{a\}$.
 
-Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$, hence a local base for $x$. But if $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.
+Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$ with respect to reverse inclusion, hence a local base for $x$.
+But if $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.

From 81ec74054dccda9b3d3f676723892f01dfcfc672 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Fri, 26 Jun 2026 08:48:54 +0100
Subject: [PATCH 06/14] Update theorems/T000909.md

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

diff --git a/theorems/T000909.md b/theorems/T000909.md
index f399faca3..5fcb4dd05 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -9,7 +9,9 @@ then:
   P000028: true
 ---
 
-Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$). Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$; by $T_1$, we can choose some $U_A \in \mathcal{U}$ with $U_A \subseteq A \setminus \{a\}$.
+Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$).
+Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$.
+By {P2} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.
 
 Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$ with respect to reverse inclusion, hence a local base for $x$.
 But if $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.

From 06639c04e4d1f9fd3bc8a5e015e654b2fa881e93 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Fri, 26 Jun 2026 08:52:16 +0100
Subject: [PATCH 07/14] Update theorems/T000910.md

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

diff --git a/theorems/T000910.md b/theorems/T000910.md
index 6f0828ff7..b718f7def 100644
--- a/theorems/T000910.md
+++ b/theorems/T000910.md
@@ -8,6 +8,10 @@ then:
   P000057: true
 ---
 
-Let $x \in X$ and $\mathcal{V}$ be a countable local $\pi$-base around $x$. Set $W = \bigcup\{X \setminus V: V \in \mathcal{V}\}$. For any $y \neq x$, $X \setminus \{y\}$ is a neighbourhood of $x$ and so there is $V \in \mathcal{V}$ with $V \subseteq X \setminus \{y\}$. Therefore $y \in X \setminus V \subseteq W$ so, since $y$ was arbitrary, $X \setminus \{x\} \subseteq W$. But $W$ is a countable union of finite sets, so $W$ is countable, so $X$ is countable.
+Let $x \in X$ and let $\mathcal{V}$ be a countable local $\pi$-base around $x$.
+The complement of every $V\in\mathcal V$ is finite; so $W := \bigcup\{X \setminus V: V \in \mathcal{V}\}$ is countable.
+For any point $y \neq x$, $X \setminus \{y\}$ is a neighbourhood of $x$ and so there is some $V \in \mathcal{V}$ with $V \subseteq X \setminus \{y\}$.
+Therefore $y \in X \setminus V \subseteq W$.
+It follows that $X \setminus \{x\} \subseteq W$ and $X$ is countable.
 
 Observe that the above argument only requires some point to have a countable local $\pi$-base, not every point.

From 107427cf73fdc8c0b7552a434ca7fc539bd6c11e Mon Sep 17 00:00:00 2001
From: JSMassmann <sylvie@83c.nl>
Date: Fri, 26 Jun 2026 09:21:07 +0100
Subject: [PATCH 08/14] Weaken some hypotheses, remove unneeded remark & add
 almost discrete + countably tight => has countable pi-character

---
 theorems/T000908.md |  4 ++--
 theorems/T000909.md |  4 ++--
 theorems/T000910.md |  2 --
 theorems/T000911.md | 11 +++++++++++
 4 files changed, 15 insertions(+), 6 deletions(-)
 create mode 100644 theorems/T000911.md

diff --git a/theorems/T000908.md b/theorems/T000908.md
index b0ed0c325..9756790a7 100644
--- a/theorems/T000908.md
+++ b/theorems/T000908.md
@@ -3,9 +3,9 @@ uid: T000908
 if:
   and:
   - P000203: true
-  - P000026: true
+  - P000029: true
 then:
   P000057: true
 ---
 
-Letting $x$ be the only point which is not isolated, and $Y$ be a countable dense set, for every $y \neq x$, $\{y\}$ is nonempty and open, so $\{y\} \cap Y \neq \emptyset$, so $y \in Y$. Therefore $X \setminus \{x\} \subseteq Y$, so $X \setminus \{x\}$ is countable, so $X$ is countable.
+Letting $x$ be the only point which is not isolated, $\{y\}$ is nonempty and open for every $y \neq x$. Since $\{\{y\}: y \neq x\}$ is a family of pairwise disjoint open sets, it is countable, so $X \setminus \{x\}$ and hence $X$ are countable.
diff --git a/theorems/T000909.md b/theorems/T000909.md
index 5fcb4dd05..4c135a019 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -4,14 +4,14 @@ if:
   and:
   - P000174: true
   - P000244: true
-  - P000002: true
+  - P000135: true
 then:
   P000028: true
 ---
 
 Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$).
 Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$.
-By {P2} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.
+By {P135} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.
 
 Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$ with respect to reverse inclusion, hence a local base for $x$.
 But if $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.
diff --git a/theorems/T000910.md b/theorems/T000910.md
index b718f7def..5fd8063e2 100644
--- a/theorems/T000910.md
+++ b/theorems/T000910.md
@@ -13,5 +13,3 @@ The complement of every $V\in\mathcal V$ is finite; so $W := \bigcup\{X \setminu
 For any point $y \neq x$, $X \setminus \{y\}$ is a neighbourhood of $x$ and so there is some $V \in \mathcal{V}$ with $V \subseteq X \setminus \{y\}$.
 Therefore $y \in X \setminus V \subseteq W$.
 It follows that $X \setminus \{x\} \subseteq W$ and $X$ is countable.
-
-Observe that the above argument only requires some point to have a countable local $\pi$-base, not every point.
diff --git a/theorems/T000911.md b/theorems/T000911.md
new file mode 100644
index 000000000..0c76f840e
--- /dev/null
+++ b/theorems/T000911.md
@@ -0,0 +1,11 @@
+---
+uid: T000911
+if:
+  and:
+  - P000203: true
+  - P000081: true
+then:
+  P000244: true
+---
+
+Let $p$ be the point so that all points other than $p$ are isolated. Since $p$ is not isolated, $X \setminus \{p\}$ is dense so $p \in \overline{X \setminus \{p\}}$. Let $D \subseteq X \setminus \{p\}$ be countable with $p \in \overline{D}$. Then $\{\{x\}: x \in D\}$ forms a countable local $\pi$-base for $p$.

From 0aec936fa87f61f7944fb11c75aa916dd23bd026 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Sat, 27 Jun 2026 10:56:37 +0100
Subject: [PATCH 09/14] Update theorems/T000908.md

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

diff --git a/theorems/T000908.md b/theorems/T000908.md
index 9756790a7..0597188f0 100644
--- a/theorems/T000908.md
+++ b/theorems/T000908.md
@@ -8,4 +8,6 @@ then:
   P000057: true
 ---
 
-Letting $x$ be the only point which is not isolated, $\{y\}$ is nonempty and open for every $y \neq x$. Since $\{\{y\}: y \neq x\}$ is a family of pairwise disjoint open sets, it is countable, so $X \setminus \{x\}$ and hence $X$ are countable.
+Let $p$ be the unique non-isolated point.
+By {P29}, $X$ has countably many isolated points.
+Therefore $X\setminus\{p\}$ is countable, and so is $X$.

From 87d1958abd5e56c18697851fdbd6286f1bf78c38 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Sat, 27 Jun 2026 11:01:21 +0100
Subject: [PATCH 10/14] Update theorems/T000909.md

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

diff --git a/theorems/T000909.md b/theorems/T000909.md
index 4c135a019..85b8f6c4f 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -14,4 +14,4 @@ Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$.
 By {P135} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.
 
 Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$ with respect to reverse inclusion, hence a local base for $x$.
-But if $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.
+If $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.

From c66babb89aca935e1777f492e5e2d8b6268a5d90 Mon Sep 17 00:00:00 2001
From: JSMassmann <sylvie@83c.nl>
Date: Sat, 27 Jun 2026 22:07:53 +0100
Subject: [PATCH 11/14] Fix wording on T909, add T912

---
 theorems/T000909.md |  6 +++++-
 theorems/T000912.md | 11 +++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 theorems/T000912.md

diff --git a/theorems/T000909.md b/theorems/T000909.md
index 85b8f6c4f..159ebac02 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -9,9 +9,13 @@ then:
   P000028: true
 ---
 
+Below is a proof that uses {P2} instead of {P135}:
+
 Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$).
 Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$.
-By {P135} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.
+By {P2} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.
 
 Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$ with respect to reverse inclusion, hence a local base for $x$.
 If $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.
+
+By passing to Kolmogorov quotients and appealing to metaproperties, the theorem holds with only {P135}.
diff --git a/theorems/T000912.md b/theorems/T000912.md
new file mode 100644
index 000000000..897c52c76
--- /dev/null
+++ b/theorems/T000912.md
@@ -0,0 +1,11 @@
+---
+uid: T000912
+if:
+  and:
+  - P000203: true
+  - P000167: false
+then:
+  P000244: true
+---
+
+Let $p$ be the unique non-isolated point. Fix a convergent non-eventually constant sequence $(s_n: n \in \mathbb{N})$. Necessarily, its limit is $p$. By passing to a subsequence, we may assume $s_n \neq p$ for all $n$. Then $\{\{s_n\}: n \in \mathbb{N}\}$ is a countable local $\pi$-base for $p$.

From 79113aeb3778c34b375d45465492cf0f64c4a83f Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Sun, 28 Jun 2026 18:00:10 +0100
Subject: [PATCH 12/14] Update theorems/T000909.md

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

diff --git a/theorems/T000909.md b/theorems/T000909.md
index 159ebac02..b6ff37300 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -17,5 +17,6 @@ By {P2} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $
 
 Clearly, $\{U_A: A \in \mathcal{A}\}$ is a countable family of neighbourhoods of $x$; we show that it is cofinal in $\mathcal{U}$ with respect to reverse inclusion, hence a local base for $x$.
 If $U \in \mathcal{U}$, there is $A \in \mathcal{A}$ with $A \subseteq U$, but since $A \not \subseteq U_A$, we cannot have $U \subseteq U_A$. By the hypothesis that $\mathcal{U}$ is linearly ordered by inclusion, we must have $U_A \subset U$ instead.
+This concludes the proof for the {P2} case.
 
-By passing to Kolmogorov quotients and appealing to metaproperties, the theorem holds with only {P135}.
+The general case with {P135} instead of {P2} follows by passing to the Kolmogorov quotient.

From e76049c52117766e3ec6b35d6968733a3c97c104 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Sun, 28 Jun 2026 18:00:20 +0100
Subject: [PATCH 13/14] Update theorems/T000909.md

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

diff --git a/theorems/T000909.md b/theorems/T000909.md
index b6ff37300..aa1bfcd71 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -9,8 +9,7 @@ then:
   P000028: true
 ---
 
-Below is a proof that uses {P2} instead of {P135}:
-
+We first handle the case where $X$ is {P2}.
 Fix some point $x$; we wish to find a countable local base for $x$. Let $\mathcal{U}$ be a local base for $x$, linearly ordered by inclusion, and $\mathcal{A}$ be a countable local $\pi$-base for $x$. WLOG assume $x$ is not isolated (otherwise $\{\{x\}\}$ is a countable local base for $x$).
 Therefore, for any $A \in \mathcal{A}$, there is some $a \in A \setminus \{x\}$.
 By {P2} we can choose some $U_A\in\mathscr U$ that avoids the point $a$; hence $A\not\subseteq U_A$.

From aeaa96002de883ee373db8c57ced51faadbbccc2 Mon Sep 17 00:00:00 2001
From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com>
Date: Sun, 28 Jun 2026 18:00:49 +0100
Subject: [PATCH 14/14] Update theorems/T000911.md

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

diff --git a/theorems/T000911.md b/theorems/T000911.md
index 0c76f840e..dd90680d4 100644
--- a/theorems/T000911.md
+++ b/theorems/T000911.md
@@ -8,4 +8,6 @@ then:
   P000244: true
 ---
 
-Let $p$ be the point so that all points other than $p$ are isolated. Since $p$ is not isolated, $X \setminus \{p\}$ is dense so $p \in \overline{X \setminus \{p\}}$. Let $D \subseteq X \setminus \{p\}$ be countable with $p \in \overline{D}$. Then $\{\{x\}: x \in D\}$ forms a countable local $\pi$-base for $p$.
+Let $p$ be the unique non-isolated point.
+Then $p \in \overline{X \setminus \{p\}}$.
+Let $D \subseteq X \setminus \{p\}$ be countable with $p \in \overline{D}$. Then $\{\{x\}: x \in D\}$ forms a countable local $\pi$-base for $p$.