diff --git a/theorems/T000908.md b/theorems/T000908.md
new file mode 100644
index 000000000..0597188f0
--- /dev/null
+++ b/theorems/T000908.md
@@ -0,0 +1,13 @@
+---
+uid: T000908
+if:
+  and:
+  - P000203: true
+  - P000029: true
+then:
+  P000057: true
+---
+
+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$.
diff --git a/theorems/T000909.md b/theorems/T000909.md
new file mode 100644
index 000000000..aa1bfcd71
--- /dev/null
+++ b/theorems/T000909.md
@@ -0,0 +1,21 @@
+---
+uid: T000909
+if:
+  and:
+  - P000174: true
+  - P000244: true
+  - P000135: true
+then:
+  P000028: true
+---
+
+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$.
+
+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.
+
+The general case with {P135} instead of {P2} follows by passing to the Kolmogorov quotient.
diff --git a/theorems/T000910.md b/theorems/T000910.md
new file mode 100644
index 000000000..5fd8063e2
--- /dev/null
+++ b/theorems/T000910.md
@@ -0,0 +1,15 @@
+---
+uid: T000910
+if:
+  and:
+  - P000222: true
+  - P000244: true
+then:
+  P000057: true
+---
+
+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.
diff --git a/theorems/T000911.md b/theorems/T000911.md
new file mode 100644
index 000000000..dd90680d4
--- /dev/null
+++ b/theorems/T000911.md
@@ -0,0 +1,13 @@
+---
+uid: T000911
+if:
+  and:
+  - P000203: true
+  - P000081: true
+then:
+  P000244: true
+---
+
+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$.
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$.