Strengthen T664 (Monotonically normal ⇒ Shrinking)

properties/P000154.md

@@ -24,6 +24,8 @@ and every point has a local base of order-convex neighborhoods.
 
 Equivalently, $X$ is homeomorphic to a subspace of a {P133}.
 
+Equivalently, $X$ is homeomorphic to a closed subspace of a {P133}.
+
 For more details and the proof of these equivalences, see {{zb:0228.54026}} (<https://eudml.org/doc/268514>)
 and {{mathse:4917398}}.
 

theorems/T000664.md

@@ -14,3 +14,7 @@ refs:
 See Theorems 1.2 and 2.3 of Chapter 17 of {{doi:10.1016/C2009-0-12309-7}}.
 
 See also {{mathse:5012078}} for a more detailed explanation.
+
+Compare with {T805} and {T543}, which constitute a refinement of this result.
+
+<!-- This theorem is kept for accessibility reasons, see https://github.com/pi-base/data/pull/1455. -->

theorems/T000805.md

@@ -0,0 +1,14 @@
+---
+uid: T000805
+if:
+  P000109: true
+then:
+  P000193: true
+refs:
+  - zb: "0769.54022"
+    name: Monotone normality (Balogh & Rudin)
+  - zb: "0761.54022"
+    name: The shrinking property and the B-property in ordered spaces (Kemoto)
+---
+
+See corollary 2.2 of {{zb:0769.54022}}. The proof for {P154} is corollary 2.2 in {{zb:0761.54022}}.