diff --git a/theorems/T000087.md b/theorems/T000087.md
index 75aa1e96e6..56ebdb7ec6 100644
--- a/theorems/T000087.md
+++ b/theorems/T000087.md
@@ -3,16 +3,7 @@ uid: T000087
 if:
   P000040: true
 then:
-  P000060: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9
-  name: Counterexamples in Topology
+  P000218: true
 ---
 
-Let \(f:X \rightarrow \mathbb{R}\) be continuous. Since for all \(a,b\in f(X)\),
-\(f^{-1}(a)\) and \(f^{-1}(b)\) are closed subsets of \(X\) and thus cannot
-be disjoint, it follows that \(a=b\), making \(f\) constant.
-
-Page 23 of {{doi:10.1007/978-1-4612-6290-9}} points out the lack of multiple
-closed singletons, forcing continuous maps from an ultraconnected space
-to any \(T_1\) space to be constant.
+By definition.
diff --git a/theorems/T000400.md b/theorems/T000400.md
index f3519762c3..5977160daf 100644
--- a/theorems/T000400.md
+++ b/theorems/T000400.md
@@ -2,12 +2,10 @@
 uid: T000400
 if:
   and:
-    - P000036: true
-    - P000085: true
+  - P000036: true
+  - P000217: true
 then:
   P000060: true
 ---
 
-The case of the empty space is obvious.
-Assume $X$ is a nonempty, connected and basically disconnected space. Let $f:X\to \mathbb R$ be a continuous function. For arbitrary $x\in X$ and $\varepsilon>0$ define $g_{x,\varepsilon}(y)=f(y)-f(x)+\varepsilon$.
-Then the set $A =\overline{\{y\in X: g_{x,\varepsilon}(y)>0\}}$ is nonempty clopen and hence equals $X$. Since $X=A\subset g_{x,\varepsilon}^{-1}([0,+\infty))$, we have $f(y)\geq f(x)-\varepsilon$ for any $x,y\in X$ and $\varepsilon>0$, implying that $f$ is constant.
+Suppose $X$ is {P217} and suppose that $f:X\to \mathbb{R}$ is a non-constant continuous function, say $f(x)\neq f(y)$. Then $Z_1 = f^{-1}(f(x))$ and $Z_2 = f^{-1}(f(y))$ are disjoint non-empty zero-sets, and so there exists a clopen set $U$ with $Z_1\subseteq U$ and $Z_2\cap U=\empty$. Since $U$ is a non-empty proper subset of $X$, $X$ is not {P36}.
diff --git a/theorems/T000768.md b/theorems/T000768.md
new file mode 100644
index 0000000000..5d67918a49
--- /dev/null
+++ b/theorems/T000768.md
@@ -0,0 +1,11 @@
+---
+uid: T000768
+if:
+  and:
+  - P000009: true
+  - P000217: true
+then:
+  P000048: true
+---
+
+If $x\neq y$ then since $X$ is functionally Hausdorff there exist disjoint zero-sets $Z_1, Z_2$ such that $x\in Z_1$ and $y\in Z_2$. Since $X$ is strongly zero-dimensional there exist disjoint clopen sets $U_1, U_2$ such that $x\in Z_1\subseteq U_1$ and $y\in Z_2\subseteq U_2$, so $X$ is totally separated.
diff --git a/theorems/T000769.md b/theorems/T000769.md
new file mode 100644
index 0000000000..bedcaa275e
--- /dev/null
+++ b/theorems/T000769.md
@@ -0,0 +1,11 @@
+---
+uid: T000769
+if:
+  and:
+  - P000036: true
+  - P000218: true
+then:
+  P000040: true
+---
+
+If there were disjoint non-empty closed sets $A_1, A_2\subseteq X$, find a clopen set $U$ with $A_1\subseteq U$ and $A_2\cap U = \emptyset$. Then $U$ is a non-empty proper clopen subset of $X$, which contradicts that $X$ is {P36}.