From c6d2ea9618e391d98ae1a5f37443d8f95d35795f Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Tue, 27 Jan 2026 20:06:44 -0500
Subject: [PATCH 1/4] Locally orderable spaces are radial

---
 properties/P000172.md |  4 ++++
 theorems/T000774.md   | 14 ++++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 theorems/T000774.md

diff --git a/properties/P000172.md b/properties/P000172.md
index 53dba5c78b..d600a1e90a 100644
--- a/properties/P000172.md
+++ b/properties/P000172.md
@@ -19,3 +19,7 @@ Compare with {P80}.
 
 - This property is hereditary.
 - $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
+- A space that is locally {P172} (every point has a neighborhood with the property)
+has the property.
+- This property is not preserved by products
+(Example: {S78|P172}).
diff --git a/theorems/T000774.md b/theorems/T000774.md
new file mode 100644
index 0000000000..f75f5747ed
--- /dev/null
+++ b/theorems/T000774.md
@@ -0,0 +1,14 @@
+---
+uid: T000774
+if:
+  P000120: true
+then:
+  P000172: true
+---
+
+Let $A\subseteq X$ and $p\in\overline A$.
+Since $X$ is {P120}, $p$ has an open neighborhood $U$
+that is orderable ({P133}), and hence also {P172}
+[(Explore)](https://topology.pi-base.org/spaces?q=LOTS%2B%7ERadial).
+Because $p\in\overline{A\cap U}$, and thus $p\in\text{cl}_U(A\cap U)$,
+it follows that there is a transfinite sequence of points of $A\cap U$ converging to $p$.

From cd9f80a77814abbb6938e47b437a9fcc11adb840 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Tue, 27 Jan 2026 23:05:09 -0500
Subject: [PATCH 2/4] renumber thm

---
 theorems/{T000774.md => T000839.md} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename theorems/{T000774.md => T000839.md} (97%)

diff --git a/theorems/T000774.md b/theorems/T000839.md
similarity index 97%
rename from theorems/T000774.md
rename to theorems/T000839.md
index f75f5747ed..ad0b34ffc5 100644
--- a/theorems/T000774.md
+++ b/theorems/T000839.md
@@ -1,5 +1,5 @@
 ---
-uid: T000774
+uid: T000839
 if:
   P000120: true
 then:

From 4aa47a5c9b2992a9e47263329f76154207b63c62 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Tue, 27 Jan 2026 23:31:38 -0500
Subject: [PATCH 3/4] simplification

---
 theorems/T000839.md | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/theorems/T000839.md b/theorems/T000839.md
index ad0b34ffc5..bb772d2e3f 100644
--- a/theorems/T000839.md
+++ b/theorems/T000839.md
@@ -6,9 +6,6 @@ then:
   P000172: true
 ---
 
-Let $A\subseteq X$ and $p\in\overline A$.
-Since $X$ is {P120}, $p$ has an open neighborhood $U$
-that is orderable ({P133}), and hence also {P172}
+This follows from the fact that {P172} is a "local" property,
+and {P133} spaces are {P172}
 [(Explore)](https://topology.pi-base.org/spaces?q=LOTS%2B%7ERadial).
-Because $p\in\overline{A\cap U}$, and thus $p\in\text{cl}_U(A\cap U)$,
-it follows that there is a transfinite sequence of points of $A\cap U$ converging to $p$.

From 3280c4f5e31c3784b060d974378c3545fe2c36fb Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Thu, 29 Jan 2026 16:23:23 -0500
Subject: [PATCH 4/4] simplification

---
 properties/P000172.md | 3 +--
 theorems/T000839.md   | 3 +--
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/properties/P000172.md b/properties/P000172.md
index d600a1e90a..545886d9a2 100644
--- a/properties/P000172.md
+++ b/properties/P000172.md
@@ -19,7 +19,6 @@ Compare with {P80}.
 
 - This property is hereditary.
 - $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
-- A space that is locally {P172} (every point has a neighborhood with the property)
-has the property.
+- If each point has a neighborhood with the property, $X$ also has the property.
 - This property is not preserved by products
 (Example: {S78|P172}).
diff --git a/theorems/T000839.md b/theorems/T000839.md
index bb772d2e3f..e7b94975eb 100644
--- a/theorems/T000839.md
+++ b/theorems/T000839.md
@@ -6,6 +6,5 @@ then:
   P000172: true
 ---
 
-This follows from the fact that {P172} is a "local" property,
-and {P133} spaces are {P172}
+Each point has a neighborhood that is {P133} and hence {P172}
 [(Explore)](https://topology.pi-base.org/spaces?q=LOTS%2B%7ERadial).