diff --git a/spaces/S000136/properties/P000019.md b/spaces/S000136/properties/P000019.md
index 28cff145e9..711c767895 100644
--- a/spaces/S000136/properties/P000019.md
+++ b/spaces/S000136/properties/P000019.md
@@ -2,9 +2,6 @@
 space: S000136
 property: P000019
 value: false
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
 ---
 
 Closed subspaces of {P19} spaces are {P19}, but the closed subspace {S137} of this space is not {P19}.
diff --git a/spaces/S000136/properties/P000051.md b/spaces/S000136/properties/P000051.md
new file mode 100644
index 0000000000..5dcb169b0a
--- /dev/null
+++ b/spaces/S000136/properties/P000051.md
@@ -0,0 +1,9 @@
+---
+space: S000136
+property: P000051
+value: true
+---
+
+For $r \in \mathbb{R}$ consider $U_r := \{f \in 2^\mathbb{R} \to 2\mid f(\{r\})=1\} \subseteq X$. Note that $U_r$ is open in the product topology and therefore open in $X$. Furthermore $U_r \cap M = \{x_r\}$, so $x_r$ is isolated in $M$ and thus $M$ is discrete as a subspace.
+
+Hence, if $A \subseteq X$ contains no elements of $X \setminus M$ we are done, otherwise $A$ already contains an isolated point by definition.
diff --git a/spaces/S000136/properties/P000139.md b/spaces/S000136/properties/P000139.md
deleted file mode 100644
index 7fc389e629..0000000000
--- a/spaces/S000136/properties/P000139.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000136
-property: P000139
-value: true
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
----
-
-Every point in $X\setminus M$ is isolated by definition.
diff --git a/spaces/S000137/properties/P000051.md b/spaces/S000137/properties/P000051.md
new file mode 100644
index 0000000000..051baf3622
--- /dev/null
+++ b/spaces/S000137/properties/P000051.md
@@ -0,0 +1,7 @@
+---
+space: S000137
+property: P000051
+value: true
+---
+
+$X$ is a subspace of {S136} and {S136|P51}.