Add actual proof for T909

Author: JSMassmann

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.