diff --git a/spaces/S000060/properties/P000032.md b/spaces/S000060/properties/P000032.md
deleted file mode 100644
index 5bd56ca4e..000000000
--- a/spaces/S000060/properties/P000032.md
+++ /dev/null
@@ -1,16 +0,0 @@
----
-space: S000060
-property: P000032
-value: false
----
-
-Take any countable partition $\{A_n:n<\omega\}$ of $\mathbb R\setminus\mathbb Q$ into Euclidean-dense subsets.
-Then $\mathscr U:=\{A_n\cup\mathbb Q: n<\omega\}$ is
-a countable open cover of $X$. Let $\mathscr V$ be an open refinement of $\mathscr U$.
-Let $U$ be any neighbourhood of $x\in\mathbb R\setminus\mathbb Q$. The closure of $U$ contains an
-interval around $x$, hence for each $n<\omega$ there exists
-$a_n\in A_n\cap \overline{U}$.
-If $a_n\in V\in\mathscr V$, the open set $V$ intersects $U$.
-Note that each $a_n$ is contained in a different element of $\mathscr V$.
-Therefore $U$ intersects infinitely many elements of $\mathscr V$,
-proving $\mathscr V$ is not locally finite.
diff --git a/spaces/S000070/properties/P000032.md b/spaces/S000070/properties/P000032.md
deleted file mode 100644
index 1a7131dd9..000000000
--- a/spaces/S000070/properties/P000032.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000070
-property: P000032
-value: false
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
----
-
-See item #8 for space #78 in {{zb:0386.54001}}.
diff --git a/spaces/S000074/properties/P000032.md b/spaces/S000074/properties/P000032.md
deleted file mode 100644
index 380aabcb6..000000000
--- a/spaces/S000074/properties/P000032.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000074
-property: P000032
-value: false
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
----
-
-See item #7 for space #82 in {{zb:0386.54001}}.
diff --git a/theorems/T000838.md b/theorems/T000838.md
new file mode 100644
index 000000000..31492b7a6
--- /dev/null
+++ b/theorems/T000838.md
@@ -0,0 +1,18 @@
+---
+uid: T000838
+if:
+  and:
+  - P000026: true
+  - P000227: true
+then:
+  P000032: false
+refs:
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+  - zb: "1116.54006"
+    name: Normality and countable paracompactness of hyperspaces of ordinals. (Kemoto, Nobuyuki)
+---
+
+See Exercise 5.2.C(b) in {{zb:0684.54001}}.
+
+See also Claim in {{zb:1116.54006}}.