diff --git a/properties/P000090.md b/properties/P000090.md
index 511f5d1a6..391805ba9 100644
--- a/properties/P000090.md
+++ b/properties/P000090.md
@@ -17,6 +17,7 @@ This is equivalent to each of the following:
 
 * An arbitrary union of closed sets is closed.
 * Each $x \in X$ has a smallest neighborhood.
+* For each $x \in X$, the *neighborhood kernel of $x$*, i. e. $\bigcap\big\{U\text{ open in }X\mid x\in U\big\}$, is open.
 * $X$ is *finitely generated*:
 For each $A \subseteq X$, $A$ is open iff $A \cap Y$ is open in the subspace $Y$ for each finite $Y \subseteq X$.
 * There is a preorder (i.e., a reflexive and transitive relation) $\preceq$ on $X$ such that the open sets are precisely the upward closed sets (i.e., sets $A\subseteq X$ such that $x\in A$ and $x\preceq y$ imply $y\in A$).
diff --git a/theorems/T000894.md b/theorems/T000894.md
new file mode 100644
index 000000000..27f64dcec
--- /dev/null
+++ b/theorems/T000894.md
@@ -0,0 +1,18 @@
+---
+uid: T000894
+if:
+  and:
+  - P000093: true
+  - P000147: true
+then:
+  P000090: true
+---
+
+Let $x \in X$ and let $A=\bigcap\{U\text{ open in }X: x\in U\}$ be the neighborhood kernel of $x$.
+We need to show that $A$ is open in $X$.
+
+Take a countable open neighborhood $V$ of $x$.
+For each $y\in V\setminus A$ there is an open neighborhood $U_y$ of $x$ not containing $y$.
+Since $V$ is countable, the countable intersection
+$V\cap\bigcap\{U_y: y\in V\setminus A\}$ is open by {P147}.
+And that intersection is equal to $A$.