Remove circular dependency between T851 and T852

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}.

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.

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$.