diff --git a/spaces/S000015/properties/P000016.md b/spaces/S000015/properties/P000016.md
deleted file mode 100644
index d797637ad6..0000000000
--- a/spaces/S000015/properties/P000016.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-space: S000015
-property: P000016
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-If $\mathcal{U}$ is an open cover an $U \in \mathcal{U}$, then $X \setminus U$ is finite, and can be covered by finitely other members of $\mathcal{U}$.
-
-See item #2 for space #18 in {{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000015/properties/P000130.md b/spaces/S000015/properties/P000130.md
deleted file mode 100644
index 4b39296959..0000000000
--- a/spaces/S000015/properties/P000130.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000015
-property: P000130
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-As stated in item #2 for space #18 in {{doi:10.1007/978-1-4612-6290-9_6}} every subset of $X$ is compact.  Hence every neighborhood of every point is compact and every point has a local base of compact neighborhoods.
diff --git a/spaces/S000015/properties/P000208.md b/spaces/S000015/properties/P000208.md
new file mode 100644
index 0000000000..79a2febdeb
--- /dev/null
+++ b/spaces/S000015/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000015
+property: P000208
+value: true
+---
+
+The closed sets satisfy the descending chain condition, because all closed sets are finite except $X$.
diff --git a/spaces/S000016/properties/P000016.md b/spaces/S000016/properties/P000016.md
deleted file mode 100644
index 49607cb6bb..0000000000
--- a/spaces/S000016/properties/P000016.md
+++ /dev/null
@@ -1,11 +0,0 @@
----
-space: S000016
-property: P000016
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-
-See item #7 for space #19 in {{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000016/properties/P000130.md b/spaces/S000016/properties/P000130.md
deleted file mode 100644
index 4101e3f645..0000000000
--- a/spaces/S000016/properties/P000130.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000016
-property: P000130
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-As stated in item #2 for space #19 in {{doi:10.1007/978-1-4612-6290-9_6}} every subset of $X$ is compact.  Hence every neighborhood of every point is compact and every point has a local base of compact neighborhoods.
diff --git a/spaces/S000016/properties/P000208.md b/spaces/S000016/properties/P000208.md
new file mode 100644
index 0000000000..05b0d4fd42
--- /dev/null
+++ b/spaces/S000016/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000016
+property: P000208
+value: true
+---
+
+The closed sets satisfy the descending chain condition, because all closed sets are finite except $X$.
diff --git a/spaces/S000019/properties/P000208.md b/spaces/S000019/properties/P000208.md
new file mode 100644
index 0000000000..88bde9c296
--- /dev/null
+++ b/spaces/S000019/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000019
+property: P000208
+value: false
+---
+
+The closed sets different from $X$ are exactly the compact sets in {S25}. However, they don't satisfy the descending chain condition: we have $Y_1 \supsetneq Y_2 \supsetneq \cdots$ where $Y_n = \left\{ 0, \frac 1n, \frac 1 {n + 1}, \frac 1 {n + 2}, \dots \right\}$.
diff --git a/spaces/S000045/properties/P000208.md b/spaces/S000045/properties/P000208.md
new file mode 100644
index 0000000000..6f63c5ebc5
--- /dev/null
+++ b/spaces/S000045/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000045
+property: P000208
+value: false
+---
+
+$\left[ -1, \frac n {n + 1} \right)$ is a strictly increasing sequence of open sets.
diff --git a/spaces/S000048/properties/P000016.md b/spaces/S000048/properties/P000016.md
deleted file mode 100644
index 51528a89da..0000000000
--- a/spaces/S000048/properties/P000016.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-space: S000048
-property: P000016
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-The complement of any open set in $X$ is finite.
-
-See item #4 for space #56 in {{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000048/properties/P000208.md b/spaces/S000048/properties/P000208.md
new file mode 100644
index 0000000000..4badcb7de8
--- /dev/null
+++ b/spaces/S000048/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000048
+property: P000208
+value: true
+---
+
+The closed sets satisfy the descending chain condition, because all closed sets are finite except $X$.
diff --git a/spaces/S000150/properties/P000208.md b/spaces/S000150/properties/P000208.md
new file mode 100644
index 0000000000..2b8e2ea2b3
--- /dev/null
+++ b/spaces/S000150/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000150
+property: P000208
+value: false
+---
+
+$\left[ \frac 1n, \to \right)$ is a strictly increasing sequence of open sets.
diff --git a/spaces/S000151/properties/P000208.md b/spaces/S000151/properties/P000208.md
new file mode 100644
index 0000000000..3cf0100e34
--- /dev/null
+++ b/spaces/S000151/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000151
+property: P000208
+value: false
+---
+
+$\left( \frac 1n, \to \right)$ is a strictly increasing sequence of open sets.
diff --git a/spaces/S000200/properties/P000016.md b/spaces/S000200/properties/P000016.md
deleted file mode 100644
index fc6e955724..0000000000
--- a/spaces/S000200/properties/P000016.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000200
-property: P000016
-value: true
----
-
-Any open cover must contain $\omega$.
diff --git a/spaces/S000200/properties/P000208.md b/spaces/S000200/properties/P000208.md
new file mode 100644
index 0000000000..f2a1d37a88
--- /dev/null
+++ b/spaces/S000200/properties/P000208.md
@@ -0,0 +1,7 @@
+---
+space: S000200
+property: P000208
+value: true
+---
+
+All closed sets are left rays, so every closed set except for $\omega$ is finite. This implies the descending chain condition on closed sets.
diff --git a/theorems/T000251.md b/theorems/T000251.md
index b45c574f27..eeafd73717 100644
--- a/theorems/T000251.md
+++ b/theorems/T000251.md
@@ -3,7 +3,10 @@ uid: T000251
 if:
   P000129: true
 then:
-  P000208: true
+  P000016: true
+refs:
+  - mathse: 3844039
+    name: What topological properties are trivially/vacuously satisfied by any indiscrete space?
 ---
 
-The ascending chain condition on open sets holds since there are at most two open sets.
+All open covers are finite to begin with.
diff --git a/theorems/T000651.md b/theorems/T000651.md
new file mode 100644
index 0000000000..5e9d86b62e
--- /dev/null
+++ b/theorems/T000651.md
@@ -0,0 +1,9 @@
+---
+uid: T000651
+if:
+  P000208: true
+then:
+  P000041: true
+---
+
+See [Lemma 5.9.6](https://stacks.math.columbia.edu/tag/04MF) from the Stacks project, which makes a stronger claim.
diff --git a/theorems/T000658.md b/theorems/T000658.md
new file mode 100644
index 0000000000..d601a4c6fc
--- /dev/null
+++ b/theorems/T000658.md
@@ -0,0 +1,11 @@
+---
+uid: T000658
+if:
+  and:
+  - P000016: true
+  - P000185: true
+then:
+  P000208: true
+---
+
+The ascending chain condition on open sets holds since there are only finitely many open sets.
diff --git a/theorems/T000659.md b/theorems/T000659.md
new file mode 100644
index 0000000000..540b66301d
--- /dev/null
+++ b/theorems/T000659.md
@@ -0,0 +1,13 @@
+---
+uid: T000659
+if:
+  and:
+  - P000208: true
+  - P000134: true
+then:
+  P000185: true
+---
+
+First observe that a {P208} {P3} space is {P52}, since every subset is compact, hence closed.
+
+Now, if $X$ is {P208} and {P134}, its Kolmogorov quotient is {P208} and {P3}, hence {P52}.  This is equivalent to $X$ being {P185}.
diff --git a/theorems/T000660.md b/theorems/T000660.md
new file mode 100644
index 0000000000..827c507964
--- /dev/null
+++ b/theorems/T000660.md
@@ -0,0 +1,13 @@
+---
+uid: T000660
+if:
+  and:
+  - P000203: true
+  - P000208: true
+then:
+  P000078: true
+---
+
+Let $p \in X$ be the only non-isolated point. The subspace $X \setminus \{p\}$ is {P52} and {P208},
+hence {P78} [(Explore)](https://topology.pi-base.org/spaces?q=Discrete+%2B+Noetherian+%2B+%7EFinite).
+Therefore $X$ is also {P78}.