Update theorems/T000909.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>

Author: JSMassmann

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.