From 0da36089d30d00d6ea3407a7bc6a677fc7effecf Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Wed, 6 May 2026 03:21:43 -0400
Subject: [PATCH 1/3] Remove circular dependency between T851 and T852

---
 theorems/T000850.md | 16 +++++++++-------
 theorems/T000851.md | 11 +++++++++--
 2 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/theorems/T000850.md b/theorems/T000850.md
index 2206275ddc..b160d88865 100644
--- a/theorems/T000850.md
+++ b/theorems/T000850.md
@@ -7,13 +7,15 @@ if:
 then:
   P000200: true
 refs:
-- mathse: 4965665
+- mathse: 4965496
   name: Answer to "Are path-connected LOTS also locally path-connected?"
 ---
 
-Up to homeomorphism, there are exactly 8 spaces that are {P133} and {P37}
-(see {{mathse:4965665}}).
-Five of them are {P200} because they are {P199} or {P137}
-(see [here](https://topology.pi-base.org/spaces?q=LOTS%2BPath+connected%2B%28Contractible%7CEmpty%29)).
-The remaining three are shown to be {P200} by a direct argument
-(see [here](https://topology.pi-base.org/spaces?q=LOTS%2BPath+connected%2B%7EContractible%2B%7EIndiscrete%2BSimply+connected)).
+Suppose $X$ is {P37} and a {P133} with the linear order $\le$.
+Let $f:S^1\to X$ be a continuous map.
+The image $f(S^1)$ is compact in $(X,\le)$, hence has a minimum $p$ and a maximum $q$.
+It is also connected, hence an order-convex subset of $X$.
+Therefore $f(S^1)=[p,q]\subseteq X$.
+The interval $[p,q]$, which is path connected, is either a singleton or is homeomorphic to {S158}
+(see {{mathse:4965496}}), and hence is {P199}.
+It follows that $f$ is null-homotopic.
diff --git a/theorems/T000851.md b/theorems/T000851.md
index 81d989c244..0c5314ecda 100644
--- a/theorems/T000851.md
+++ b/theorems/T000851.md
@@ -6,5 +6,12 @@ then:
   P000229: true
 ---
 
-Each point has a neighborhood homeomorphic to a {P133}, hence {P154}.
-That neighborhood is {P229} because {T852}.
+It suffices to show that every $x\in X$ has a neighborhood that is {P229}.
+There is an open neighborhood $U$ of $x$ that is a {P133} with the linear order $\le$.
+Let $V$ be a path component of $U$.
+Since a connected set in a LOTS is order-convex,
+$V$ is also a LOTS with the order $\le$ induced from $U$.
+
+Now use {T850}, which in turn implies {P229}
+[(Explore)](https://topology.pi-base.org/spaces?q=Simply+connected%2B%7ESemilocally+simply+connected),
+to conclude that $V$ has the required property, and so does $U$.

From a8593aee7eca054e6cf0bc64dd0dc19c302dc22c Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Tue, 5 May 2026 23:14:38 -0400
Subject: [PATCH 2/3] add T846: loc orderable + loc path connected => loc
 half-line

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

diff --git a/theorems/T000846.md b/theorems/T000846.md
new file mode 100644
index 0000000000..a76adabab0
--- /dev/null
+++ b/theorems/T000846.md
@@ -0,0 +1,27 @@
+---
+uid: T000846
+if:
+  and:
+  - P000120: true
+  - P000042: true
+  - P000139: false
+then:
+  P000241: true
+refs:
+- mathse: 4965496
+  name: Answer to "Are path-connected LOTS also locally path-connected?"
+---
+
+The empty space is vacuously {P241}.
+Now assume $X\ne\emptyset$ and let $x\in X$.
+There is an open neighborhood $U$ of $x$ that is orderable ({P133}),
+and a {P37} open neighborhood $V$ of $x$ with $V\subseteq U$.
+Since a connected set in a LOTS is order-convex,
+$V$ is also a LOTS with the order $\le$ induced from $U$.
+
+Take a neighborhood of $x$ in $(V,\le)$ of the form $[p,q]$ for some $p\le x\le q$;
+necessarily $p<q$ because $x$ is not isolated in $V$.
+The interval $[p,q]\subseteq V$ is homeomorphic to the interval $[0,1]\subseteq\mathbb R$
+(see {{mathse:4965496}}).
+From this, it is easy to obtain a neighborhood of $x$ homeomorphic to {S210}.
+That is, $X$ is {P241}.

From 245addb2a0967d5c8d6f484f888be015e6adbe3f Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Thu, 7 May 2026 01:31:49 -0400
Subject: [PATCH 3/3] remove some redundant traits

---
 spaces/S000038/properties/P000200.md | 14 --------------
 spaces/S000149/properties/P000200.md |  8 --------
 spaces/S000201/properties/P000122.md |  6 ------
 spaces/S000201/properties/P000200.md | 12 ------------
 4 files changed, 40 deletions(-)
 delete mode 100644 spaces/S000038/properties/P000200.md
 delete mode 100644 spaces/S000149/properties/P000200.md
 delete mode 100644 spaces/S000201/properties/P000122.md
 delete mode 100644 spaces/S000201/properties/P000200.md

diff --git a/spaces/S000038/properties/P000200.md b/spaces/S000038/properties/P000200.md
deleted file mode 100644
index 8cfe5125a7..0000000000
--- a/spaces/S000038/properties/P000200.md
+++ /dev/null
@@ -1,14 +0,0 @@
----
-space: S000038
-property: P000200
-value: true
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
----
-
-For any two points $p<q$ in $X$ the interval $[p,q]$ is homeomorphic to {S158}.
-See item #6 for space #45 in {{zb:0386.54001}}.
-It follows that $X$ is {P37}.
-
-Let $F : S^1 \to X$ be a continuous map. The image of $F$ is compact, hence bounded in $X$ as an ordered set. So $F(X)$ is contained in some interval homeomorphic to {S158}. Since {S158|P199}, $F$ is homotopic to a constant map.
diff --git a/spaces/S000149/properties/P000200.md b/spaces/S000149/properties/P000200.md
deleted file mode 100644
index b707684076..0000000000
--- a/spaces/S000149/properties/P000200.md
+++ /dev/null
@@ -1,8 +0,0 @@
----
-space: S000149
-property: P000200
-value: true
----
-
-Similar to the proof that {S38|P200}, using the same fact that 
-for any two points $p<q$ the interval $[p,q]$ is homeomorphic to {S158}.
diff --git a/spaces/S000201/properties/P000122.md b/spaces/S000201/properties/P000122.md
deleted file mode 100644
index edf048863f..0000000000
--- a/spaces/S000201/properties/P000122.md
+++ /dev/null
@@ -1,6 +0,0 @@
----
-space: S000201
-property: P000122
-value: false
----
-For any neighborhood $U$ of the point $p=(0,0)$, $U\setminus\{p\}$ has infinitely many connected components. This cannot happen in a locally Euclidean space.
diff --git a/spaces/S000201/properties/P000200.md b/spaces/S000201/properties/P000200.md
deleted file mode 100644
index 3c11f907db..0000000000
--- a/spaces/S000201/properties/P000200.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-space: S000201
-property: P000200
-value: false
-refs:
-  - zb: "1044.55001"
-    name: Algebraic Topology (Hatcher)
----
-
-Same argument as {S139|P200}.
-
-See Example 1.25 of {{zb:1044.55001}} for a comparison of $\pi_1(X)$ with the fundamental group of {S139}.