diff --git a/theorems/T000552.md b/theorems/T000552.md
index 2834aee9a..4c3be64db 100644
--- a/theorems/T000552.md
+++ b/theorems/T000552.md
@@ -8,7 +8,6 @@ if:
 then:
   P000129: true
 ---
-
 If a {P196} space is {P16}, then it must have a second largest open set 
 (otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover).
 To be {P86}, no points can lie in this second-largest set, so the space is {P129}.
diff --git a/theorems/T000553.md b/theorems/T000553.md
index 7d6bf90ad..6d31adfc9 100644
--- a/theorems/T000553.md
+++ b/theorems/T000553.md
@@ -1,14 +1,9 @@
 ---
 uid: T000553
 if:
-  and:
-  - P000001: true
-  - P000090: true
-  - P000027: true
+  P000196: true
 then:
-  P000057: true
+  P000042: 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.
+Every subset of a {P196} space is {P40}, and {T38}.
diff --git a/theorems/T000554.md b/theorems/T000554.md
index e2f808bc1..487604d1c 100644
--- a/theorems/T000554.md
+++ b/theorems/T000554.md
@@ -12,4 +12,4 @@ refs:
 - doi: 10.1017/9781316543870
   name: Spectral spaces (Dickmann, Schwartz, Tressl)
 ---
-Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}.
+Shown in Proposition 1.6.7 of {{doi:10.1017/9781316543870}}. In particular, it follows that the specialization order is order-isomorphic to a non-limit ordinal.
diff --git a/theorems/T000555.md b/theorems/T000555.md
new file mode 100644
index 000000000..4f896a3e8
--- /dev/null
+++ b/theorems/T000555.md
@@ -0,0 +1,11 @@
+---
+uid: T000555
+if:
+  and:
+  - P000196: true
+  - P000176: true
+then:
+  P000044: false
+---
+
+Since any subset is connected, any partition into non-singletons suffices.
diff --git a/theorems/T000556.md b/theorems/T000556.md
new file mode 100644
index 000000000..6d869685f
--- /dev/null
+++ b/theorems/T000556.md
@@ -0,0 +1,12 @@
+---
+uid: T000556
+if:
+  and:
+  - P000196: true
+  - P000016: true
+then:
+  P000146: true
+---
+If a {P196} space is {P16}, then it must have a second largest open set 
+(otherwise, $\mathcal T_X\setminus\{X\}$ would be totally ordered with no upper bound and therefore an open cover with no finite subcover).
+Thus, any open cover must contain $X$, so it admits a refinement containing $X$ as the only nonempty set.
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.