Fix wording on T909, add T912

Author: JSMassmann

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

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