diff --git a/properties/P000185.md b/properties/P000185.md
index 2315f680a..325c99d54 100644
--- a/properties/P000185.md
+++ b/properties/P000185.md
@@ -2,8 +2,10 @@
 uid: P000185
 name: Partition topology
 refs:
-  - doi: 10.1007/978-1-4612-6290-9
-    name: Counterexamples in Topology
+- doi: 10.1007/978-1-4612-6290-9
+  name: Counterexamples in Topology
+- doi: 10.5186/aasfm.1977.0321
+  name: On ultrapseudocompact and related spaces (T. Nieminen)
 ---
 
 Any of the following equivalent properties holds:
@@ -14,5 +16,7 @@ Any of the following equivalent properties holds:
 - The space's Kolmogorov quotient is {P52}.
 - The space is the disjoint union of a collection of {P129} spaces.
 
+For proof of the equivalences and further characterizations, see section 13 of {{doi:10.5186/aasfm.1977.0321}}.
+
 Defined as example #5 ("Partition Topology")
 in {{doi:10.1007/978-1-4612-6290-9}}.
diff --git a/properties/P000196.md b/properties/P000196.md
new file mode 100644
index 000000000..957361c34
--- /dev/null
+++ b/properties/P000196.md
@@ -0,0 +1,18 @@
+---
+uid: P000196
+name: Hereditarily connected
+aliases:
+- Totally ordered topology
+refs:
+- doi: 10.5186/aasfm.1977.0321
+  name: On ultrapseudocompact and related spaces (T. Nieminen)
+---
+
+Any of the following equivalent properties holds:
+
+- Any subspace is connected.
+- The open sets are totally ordered by inclusion.
+- The closed sets are totally ordered by inclusion.
+- The specialization preorder is total.
+
+For proof of the equivalences and further characterizations, see section 12 of {{doi:10.5186/aasfm.1977.0321}}.
diff --git a/spaces/S000187/properties/P000196.md b/spaces/S000187/properties/P000196.md
new file mode 100644
index 000000000..e29f17433
--- /dev/null
+++ b/spaces/S000187/properties/P000196.md
@@ -0,0 +1,7 @@
+---
+space: S000187
+property: P000196
+value: true
+---
+
+By construction.
diff --git a/spaces/S000199/properties/P000002.md b/spaces/S000199/properties/P000002.md
deleted file mode 100644
index e7a65eb1b..000000000
--- a/spaces/S000199/properties/P000002.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000199
-property: P000002
-value: false
----
-
-Every neighborhood of $1$ is a neighborhood of $0$.
diff --git a/spaces/S000199/properties/P000014.md b/spaces/S000199/properties/P000014.md
deleted file mode 100644
index 4d96693a4..000000000
--- a/spaces/S000199/properties/P000014.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000199
-property: P000014
-value: true
----
-
-The collection of closed sets is a chain under inclusion;
-that is,
-for each pair of closed sets, one is contained in the other.
-Therefore every subspace is vacuously {P13}.
diff --git a/spaces/S000199/properties/P000039.md b/spaces/S000199/properties/P000039.md
deleted file mode 100644
index 7edff5528..000000000
--- a/spaces/S000199/properties/P000039.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-space: S000199
-property: P000039
-value: true
----
-
-The topology is a chain under inclusion;
-that is,
-for each pair of open sets, one is contained in the other.
diff --git a/spaces/S000199/properties/P000051.md b/spaces/S000199/properties/P000051.md
new file mode 100644
index 000000000..ef0361c92
--- /dev/null
+++ b/spaces/S000199/properties/P000051.md
@@ -0,0 +1,7 @@
+---
+space: S000199
+property: P000051
+value: true
+---
+Since $\omega$ is well-ordered, a nonempty set $Y\subseteq\omega$ has a least element $\alpha$.
+Then $\alpha$ is isolated in $Y$ since $[0,\alpha+1)\cap Y=\{\alpha\}$.
diff --git a/spaces/S000199/properties/P000086.md b/spaces/S000199/properties/P000086.md
deleted file mode 100644
index 557402636..000000000
--- a/spaces/S000199/properties/P000086.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000199
-property: P000086
-value: false
----
-
-$0$ belongs to every nonempty open set, but $1$ does not belong to $(\leftarrow,0]$.
diff --git a/spaces/S000199/properties/P000136.md b/spaces/S000199/properties/P000136.md
new file mode 100644
index 000000000..cd74fca5d
--- /dev/null
+++ b/spaces/S000199/properties/P000136.md
@@ -0,0 +1,7 @@
+---
+space: S000199
+property: P000136
+value: true
+---
+
+Every infinite subspace is homeomorphic to the space itself, and any open cover not containing $\omega$ must be an infinite set of left rays and so cannot have a finite subcover.
diff --git a/spaces/S000187/properties/P000039.md b/spaces/S000199/properties/P000181.md
similarity index 52%
rename from spaces/S000187/properties/P000039.md
rename to spaces/S000199/properties/P000181.md
index 7d239f6d7..21e3c555e 100644
--- a/spaces/S000187/properties/P000039.md
+++ b/spaces/S000199/properties/P000181.md
@@ -1,6 +1,6 @@
 ---
-space: S000187
-property: P000039
+space: S000199
+property: P000181
 value: true
 ---
 
diff --git a/spaces/S000199/properties/P000196.md b/spaces/S000199/properties/P000196.md
new file mode 100644
index 000000000..cc091bd9f
--- /dev/null
+++ b/spaces/S000199/properties/P000196.md
@@ -0,0 +1,7 @@
+---
+space: S000199
+property: P000196
+value: true
+---
+
+By construction.
diff --git a/spaces/S000200/properties/P000002.md b/spaces/S000200/properties/P000002.md
deleted file mode 100644
index ea4e1784b..000000000
--- a/spaces/S000200/properties/P000002.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000200
-property: P000002
-value: false
----
-
-Every neighborhood of $0$ is a neighborhood of $1$.
diff --git a/spaces/S000200/properties/P000014.md b/spaces/S000200/properties/P000014.md
deleted file mode 100644
index b48008995..000000000
--- a/spaces/S000200/properties/P000014.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000200
-property: P000014
-value: true
----
-
-The collection of closed sets is a chain under inclusion;
-that is,
-for each pair of closed sets, one is contained in the other.
-Therefore every subspace is vacuously {P13}.
diff --git a/spaces/S000200/properties/P000016.md b/spaces/S000200/properties/P000016.md
new file mode 100644
index 000000000..fc6e95572
--- /dev/null
+++ b/spaces/S000200/properties/P000016.md
@@ -0,0 +1,7 @@
+---
+space: S000200
+property: P000016
+value: true
+---
+
+Any open cover must contain $\omega$.
diff --git a/spaces/S000200/properties/P000039.md b/spaces/S000200/properties/P000039.md
deleted file mode 100644
index ee8b420d9..000000000
--- a/spaces/S000200/properties/P000039.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-space: S000200
-property: P000039
-value: true
----
-
-The topology is a chain under inclusion;
-that is,
-for each pair of open sets, one is contained in the other.
diff --git a/spaces/S000200/properties/P000086.md b/spaces/S000200/properties/P000086.md
deleted file mode 100644
index d470218f4..000000000
--- a/spaces/S000200/properties/P000086.md
+++ /dev/null
@@ -1,8 +0,0 @@
----
-space: S000200
-property: P000086
-value: false
----
-
-$0$ belongs to only one open set $[0,\infty)$, but $1$ belongs to two open sets $[0,\rightarrow)$
-and $[1,\rightarrow)$.
diff --git a/spaces/S000187/properties/P000040.md b/spaces/S000200/properties/P000181.md
similarity index 52%
rename from spaces/S000187/properties/P000040.md
rename to spaces/S000200/properties/P000181.md
index 86b6aca72..2018d047e 100644
--- a/spaces/S000187/properties/P000040.md
+++ b/spaces/S000200/properties/P000181.md
@@ -1,6 +1,6 @@
 ---
-space: S000187
-property: P000040
+space: S000200
+property: P000181
 value: true
 ---
 
diff --git a/spaces/S000200/properties/P000196.md b/spaces/S000200/properties/P000196.md
new file mode 100644
index 000000000..d3e2d8cf9
--- /dev/null
+++ b/spaces/S000200/properties/P000196.md
@@ -0,0 +1,7 @@
+---
+space: S000200
+property: P000196
+value: true
+---
+
+By construction.
diff --git a/theorems/T000546.md b/theorems/T000546.md
new file mode 100644
index 000000000..c806a6ee6
--- /dev/null
+++ b/theorems/T000546.md
@@ -0,0 +1,9 @@
+---
+uid: T000546
+if:
+  P000196: true
+then:
+  P000039: true
+---
+
+The open sets are totally ordered by set inclusion and thus no two nonempty ones are disjoint.
diff --git a/theorems/T000547.md b/theorems/T000547.md
new file mode 100644
index 000000000..3803e584f
--- /dev/null
+++ b/theorems/T000547.md
@@ -0,0 +1,9 @@
+---
+uid: T000547
+if:
+  P000196: true
+then:
+  P000014: true
+---
+
+Any {P196} space is trivially {P13} (as there are no disjoint closed sets), so all subspaces are as well.
diff --git a/theorems/T000548.md b/theorems/T000548.md
new file mode 100644
index 000000000..eb5743d0b
--- /dev/null
+++ b/theorems/T000548.md
@@ -0,0 +1,14 @@
+---
+uid: T000548
+if:
+  and:
+  - P000039: true
+  - P000014: true
+then:
+  P000196: true
+refs:
+- doi: 10.5186/aasfm.1977.0321
+  name: On ultrapseudocompact and related spaces (T. Nieminen)
+---
+
+See condition (10) of theorem 23 at {{doi:10.5186/aasfm.1977.0321}} (reading $T_5$ as {P14}).
diff --git a/theorems/T000549.md b/theorems/T000549.md
new file mode 100644
index 000000000..69586ecab
--- /dev/null
+++ b/theorems/T000549.md
@@ -0,0 +1,9 @@
+---
+uid: T000549
+if:
+  P000196: true
+then:
+  P000174: true
+---
+
+The topology is totally ordered by inclusion, so the set of open neighborhoods of any point is as well.
diff --git a/theorems/T000550.md b/theorems/T000550.md
new file mode 100644
index 000000000..3ab1ae577
--- /dev/null
+++ b/theorems/T000550.md
@@ -0,0 +1,12 @@
+---
+uid: T000550
+if:
+  and:
+  - P000193: true
+  - P000039: true
+then:
+  P000146: true
+---
+
+In a {P39} space $X$, the closure of every nonempty open set is $X$, so any open cover that admits a shrinking must contain $X$ (as otherwise each of its open sets could only contain the closure of $\varnothing$).
+Thus, any such open cover admits an open refinement to the partition $\{X\}$.
diff --git a/theorems/T000551.md b/theorems/T000551.md
new file mode 100644
index 000000000..1c5774c8a
--- /dev/null
+++ b/theorems/T000551.md
@@ -0,0 +1,12 @@
+---
+uid: T000551
+if:
+  and:
+  - P000196: true
+  - P000093: true
+  - P000057: false
+then:
+  P000114: true
+---
+
+By {P93} choose a countable open neighborhood of each point.  So $X$ can be covered by a family of countable sets, forming a chain under inclusion by {P196}.  And the union of a chain of countable sets has cardinality at most $\aleph_1$ (see {{mathse:342091}} for example).
diff --git a/theorems/T000552.md b/theorems/T000552.md
new file mode 100644
index 000000000..532f52226
--- /dev/null
+++ b/theorems/T000552.md
@@ -0,0 +1,11 @@
+---
+uid: T000552
+if:
+  and:
+  - P000146: true
+  - P000036: true
+  - P000086: true
+then:
+  P000129: true
+---
+Any clopen partition of a {P36} space $X$ must contain $X$, so every open cover admitting a clopen partition as refinement must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so some points have $X$ as their only neighborhood. By homogeneity, this must then be true of all points, i.e. the space is {P129}.
diff --git a/theorems/T000553.md b/theorems/T000553.md
new file mode 100644
index 000000000..6d31adfc9
--- /dev/null
+++ b/theorems/T000553.md
@@ -0,0 +1,9 @@
+---
+uid: T000553
+if:
+  P000196: true
+then:
+  P000042: true
+---
+
+Every subset of a {P196} space is {P40}, and {T38}.
diff --git a/theorems/T000554.md b/theorems/T000554.md
new file mode 100644
index 000000000..fc39050ba
--- /dev/null
+++ b/theorems/T000554.md
@@ -0,0 +1,17 @@
+---
+uid: T000554
+if:
+  and:
+  - P000196: true
+  - P000016: true
+  - P000073: true
+  - P000090: true
+then:
+  P000075: true
+refs:
+- doi: 10.1017/9781316543870
+  name: Spectral spaces (Dickmann, Schwartz, Tressl)
+---
+Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}.
+
+Furthermore, if the space is nonempty, its specialization order is order-isomorphic to a successor ordinal $\lambda$ and the space is homeomorphic to $\lambda$ with the left-ray topology having the collection of intervals $[0,\alpha]$ ($\alpha\in\lambda$) as a base.
diff --git a/theorems/T000555.md b/theorems/T000555.md
new file mode 100644
index 000000000..845d480a0
--- /dev/null
+++ b/theorems/T000555.md
@@ -0,0 +1,10 @@
+---
+uid: T000555
+if:
+  and:
+  - P000196: true
+  - P000176: true
+then:
+  P000044: false
+---
+$X$ has two disjoint subsets, each with at least two points, and each of the subsets is connected.
diff --git a/theorems/T000556.md b/theorems/T000556.md
new file mode 100644
index 000000000..79a0abbd0
--- /dev/null
+++ b/theorems/T000556.md
@@ -0,0 +1,10 @@
+---
+uid: T000556
+if:
+  and:
+  - P000146: true
+  - P000036: true
+then:
+  P000020: true
+---
+Any clopen partition of a {P36} space $X$ must contain $X$, so to admit clopen refinements every open cover must contain $X$. Thus, the union of all open sets except for $X$ cannot equal $X$ (as that would be an open cover not containing $X$), so any sequence converges to all points outside of that union (whose only neighborhood is $X$).
diff --git a/theorems/T000557.md b/theorems/T000557.md
new file mode 100644
index 000000000..bd802b06c
--- /dev/null
+++ b/theorems/T000557.md
@@ -0,0 +1,14 @@
+---
+uid: T000557
+if:
+  and:
+  - P000001: true
+  - P000090: true
+  - P000027: true
+then:
+  P000057: true
+---
+
+In an {P90} space, the smallest basis is the set of smallest neighborhoods of points.
+When it is also {P1}, these are all distinct, so they are in bijection with the set of points.
+Thus, such a space has a countable basis iff it is countable.