diff --git a/properties/P000221.md b/properties/P000221.md
new file mode 100644
index 0000000000..468c3e83ca
--- /dev/null
+++ b/properties/P000221.md
@@ -0,0 +1,36 @@
+---
+uid: P000221
+name: Dieudonné complete
+aliases:
+  - Completely uniformizable
+  - Topologically complete
+refs:
+  - wikipedia: Uniform_space
+    name: Uniform space on Wikipedia
+  - wikipedia: Completely_uniformizable_space
+    name: Completely uniformizable space
+  - doi: 10.1007/978-1-4615-7819-2
+    name: Rings of Continuous Functions (Gillman & Jerison)
+  - mr: 370454
+    name: General Topology (Kelley)
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+---
+
+The topology on the space $X$ is induced by a [complete uniformity](https://en.wikipedia.org/wiki/Uniform_space#Completeness) $\mathcal{U}$.
+
+We call uniformity $\mathcal{U}$ complete if every Cauchy filter $\mathcal{F}$ on $(X, \mathcal{U})$ converges. Equivalently, every Cauchy net $(x_i)_{i\in I}$ on $(X, \mathcal{U})$ converges. Here Cauchy filter is a filter $\mathcal{F}$ such that for every $U\in\mathcal{U}$ there exists $A\in\mathcal{F}$ such that $A\times A\subseteq U$. A Cauchy net is a net $(x_i)_{i\in I}$ such that for every $U\in\mathcal{U}$ there exists $i_0$ such that $(x_j, x_k)\in U$ for $j, k\geq i_0$.
+
+If $X$ is $T_0$ this is equivalent to the following (see {{zb:0684.54001}} exercise 8.5.13a):
+
+1. $X$ is a closed subspace of a product of {P55} spaces
+2. $X$ is a closed subspace of a product of {P53} spaces.
+
+Compare with definition in 15.7 of {{doi:10.1007/978-1-4615-7819-2}} where uniform structure is defined using pseudometrics instead.
+
+This property is *topologically complete* in {{mr:370454}}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/theorems/T000386.md b/theorems/T000386.md
index 2664032d12..ab53aa24d5 100644
--- a/theorems/T000386.md
+++ b/theorems/T000386.md
@@ -3,15 +3,9 @@ uid: T000386
 if:
   and:
     - P000022: true
-    - P000162: true
+    - P000221: true
 then:
   P000016: true
-refs:
-- mathse: 4728863
-  name: Compactness, pseudocompactness, and realcompactness without Hausdorff
 ---
 
-Take the space $H\subseteq \mathbb R^\kappa$ (by {P162}); its projection $H_\alpha\subseteq\mathbb R$
-for each factor $\alpha<\kappa$ must be bounded (by {P22}), and thus $\overline{H_\alpha}$ is {P000016}
-by the [Heine-Borel theorem](https://en.wikipedia.org/wiki/Heine%E2%80%93Borel_theorem). This makes $H$
-a closed subset of the {P000016} space $\prod_{\alpha<\kappa}\overline{H_\alpha}$, and thus {P000016}.
+By taking Kolmogorov quotient we can assume $X$ is $T_0$. If $X\subseteq \prod_\alpha X_\alpha$ is closed where $X_\alpha$ are metric spaces, and $\pi_\alpha:X\to X_\alpha$ are projections, then $\pi_\alpha(X)\subseteq X_\alpha$ is {P22} and {P53}, and so {P16}. It follows that $X$ is a closed subspace of the {P16} space $\prod_\alpha \pi_\alpha(X)$, and so {P16}.
diff --git a/theorems/T000774.md b/theorems/T000774.md
new file mode 100644
index 0000000000..84d37d06e5
--- /dev/null
+++ b/theorems/T000774.md
@@ -0,0 +1,9 @@
+---
+uid: T000774
+if:
+  P000221: true
+then:
+  P000012: true
+---
+
+{P12} spaces are precisely the spaces admitting a uniformity.
diff --git a/theorems/T000775.md b/theorems/T000775.md
new file mode 100644
index 0000000000..6551d59d05
--- /dev/null
+++ b/theorems/T000775.md
@@ -0,0 +1,13 @@
+---
+uid: T000775
+if:
+  P000162: true
+then:
+  P000221: true
+refs:
+  - doi: 10.1007/978-1-4615-7819-2
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+See corollary 15.14 of {{doi:10.1007/978-1-4615-7819-2}} for complete uniformity on a {P162} space.
+Alternatively, a {P162} space is a closed subspace of product of {S25} and {S25|P53}.
diff --git a/theorems/T000776.md b/theorems/T000776.md
new file mode 100644
index 0000000000..2e5b06dd6b
--- /dev/null
+++ b/theorems/T000776.md
@@ -0,0 +1,15 @@
+---
+uid: T000776
+if:
+  and:
+  - P000001: true
+  - P000164: true
+  - P000221: true
+then:
+  P000162: true
+refs:
+  - doi: 10.1007/978-1-4615-7819-2
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+A {P221} {P1} space is {P6}. Now apply theorem 15.20 of {{doi:10.1007/978-1-4615-7819-2}}.
diff --git a/theorems/T000777.md b/theorems/T000777.md
new file mode 100644
index 0000000000..5f3f9f8d48
--- /dev/null
+++ b/theorems/T000777.md
@@ -0,0 +1,14 @@
+---
+uid: T000777
+if:
+  and:
+  - P000134: true
+  - P000030: true
+then:
+  P000221: true
+refs:
+  - mr: 370454
+    name: General Topology (Kelley)
+---
+
+By taking Kolmogorov quotient we can assume $X$ is {P3}. Assume $X$ is not {P221}. Since $X$ is {P207}, the neighbourhoods of the diagonal $\Delta_X\subseteq X\times X$ form a uniformity $\mathcal{U}$ on $X$. Equip $X$ with this uniformity and let $(x_i)_{i\in I}$ be a Cauchy net on $X$ that isn't convergent. Since a Cauchy net converges to each of its adherence points, for each $x\in X$ there exists a neighbourhood $U_x$ of $x$ such that $x_i\notin U_x$ for large enough $i$. From theorem 5.28 of {{mr:370454}}, the open cover $\{U_x : x\in X\}$ is even, so there exists $V\in\mathcal{U}$ such that $V[x] = \{y\in X :(x, y)\in V\}$ is contained in $U_z$ for some $z\in X$. If $i_0$ is such that $(x_j, x_k)\in V$ for $j, k\geq i_0$, then $(x_{i_0}, x_i)\in V$ for all $i\geq i_0$, so $x_i\in V[x_{i_0}]\subseteq U_z$ for all $i\geq i_0$. This is a contradiction since $x_i\notin U_z$ for big enough $i$.