From 09cb0a001dd414ff27ef30aefce4317100a0cb32 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Tue, 4 Aug 2026 23:25:16 -0400
Subject: [PATCH 1/2] some metaproperties

---
 properties/P000024.md | 11 ++++++++++-
 properties/P000090.md |  1 +
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/properties/P000024.md b/properties/P000024.md
index 6fe677d554..5d6c92386a 100644
--- a/properties/P000024.md
+++ b/properties/P000024.md
@@ -15,4 +15,13 @@ Each point has a local base of neighborhoods with compact closure.
 Equivalently (see Condition 2 of {{wikipedia:Locally_compact_space}}), every point in $X$ has
 a closed and compact neighborhood.
 
-Defined on page 20 of {{zb:0386.54001}} as "strongly locally compact". Contrast with {P130}.
+Defined on page 20 of {{zb:0386.54001}} as "strongly locally compact".
+
+Compare with {P130}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
+- This property is hereditary with respect to closed sets.
+- This property is preserved by finite products.
diff --git a/properties/P000090.md b/properties/P000090.md
index 391805ba93..2da66ae62d 100644
--- a/properties/P000090.md
+++ b/properties/P000090.md
@@ -28,6 +28,7 @@ See also {{zb:0944.54018}}.
 ----
 #### Meta-properties
 
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
 - This property is hereditary.
 - This property is preserved by arbitrary disjoint unions.
 - This property is preserved by finite products.

From 8c0e5185410abeb6e68c7805157ef94f5761033c Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Tue, 4 Aug 2026 23:26:03 -0400
Subject: [PATCH 2/2] CWH + loc rel compact + Alexandrov + T0 => normal

---
 theorems/T000927.md | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 theorems/T000927.md

diff --git a/theorems/T000927.md b/theorems/T000927.md
new file mode 100644
index 0000000000..38e158bb07
--- /dev/null
+++ b/theorems/T000927.md
@@ -0,0 +1,31 @@
+---
+uid: T000927
+if:
+  and:
+  - P000246: true
+  - P000024: true
+  - P000090: true
+  - P000001: true
+then:
+  P000013: true
+---
+
+We assume $X$ is {P24}, {P90}, {P1}
+and not {P13} and show it is not {P246}.
+
+*Notation*:  Write $x\le y$ when $x\in\overline{\{y\}}$ (specialization order).
+The smallest open neighborhoods of a point $a\in X$ and of a set $A\subseteq X$ are the upper sets
+${\uparrow}a:=\{x\in X:a\le x\}$ and ${\uparrow}A:=\bigcup_{a\in A}{\uparrow}a$.
+And let ${\downarrow}a:=\{x\in X:x\le a\}$.
+
+Let $A$ and $B$ be disjoint closed sets that don't have disjoint open neighborhoods.
+So ${\uparrow}A\cap{\uparrow}B\ne\emptyset$ and ${\uparrow}a\cap{\uparrow}b\ne\emptyset$
+for some $a\in A$ and $b\in B$.
+The set ${\downarrow}a$ is closed in $X$, hence {P24}.
+Since {T641}, there is a point $a_1\le a$ with $\{a_1\}$ closed in ${\downarrow}a$, hence closed in $X$.
+Similarly there is a point $b_1\le b$ with $\{b_1\}$ closed in $X$.
+The points $a_1$ and $b_1$ are distinct, because $a_1\in A$ and $b_1\in B$.
+The set $\{a_1,b_1\}$ is discrete and closed in $X$ and
+its points cannot be separated by disjoint open sets as
+${\uparrow}a_1\cap{\uparrow}b_1 \supseteq {\uparrow}a\cap{\uparrow}b\ne\emptyset$.
+This shows that $X$ is not {P246}.