diff --git a/properties/P000022.md b/properties/P000022.md
index 303afb6bcf..31209b8050 100644
--- a/properties/P000022.md
+++ b/properties/P000022.md
@@ -13,4 +13,5 @@ Defined on page 20 of {{zb:0386.54001}}.
 ----
 #### Meta-properties
 
+- $X$ satisfies this property iff its Kolmogorov quotient $\mathrm{Kol}(X)$ does.
 - This property is preserved in any coarser topology.
diff --git a/properties/P000049.md b/properties/P000049.md
index a54e17224f..2729d11097 100644
--- a/properties/P000049.md
+++ b/properties/P000049.md
@@ -4,7 +4,7 @@ name: Extremally disconnected
 refs:
   - zb: "1052.54001"
     name: General Topology (Willard)
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman & Jerison)
   - zb: "0386.54001"
     name: Counterexamples in Topology
@@ -18,7 +18,7 @@ The closure of every open set in $X$ is open or, equivalently, clopen.
 
 Equivalently, any two disjoint open sets have disjoint closures.
 
-Defined in problem 15G of {{zb:1052.54001}} and problem 1H of {{doi:10.1007/978-1-4615-7819-2}}.
+Defined in problem 15G of {{zb:1052.54001}} and problem 1H of {{zb:1380.46022}}.
 
 {{zb:0386.54001}} defines it on page 32 with the additional assumption of {P3},
 which we do not assume here.
diff --git a/properties/P000055.md b/properties/P000055.md
index 982f8b96ce..8ac9097f37 100644
--- a/properties/P000055.md
+++ b/properties/P000055.md
@@ -16,8 +16,9 @@ that is, a metric for which every Cauchy sequence converges.
 A sequence $(x_n)_n$ is *Cauchy* provided for each distance $\epsilon>0$, there is
 a natural number $N$ for which $d(x_i,x_j)<\epsilon$ for all $i,j>N$.
 
-See Definition 24.2 in {{zb:1052.54001}}.
-Defined on page 37 of {{zb:0386.54001}} as "topologically complete".
+Defined in 24.2 of {{zb:1052.54001}}.
+Called *topologically complete* on page 37 of {{zb:0386.54001}};
+this last term has also been used for {P63} and {P221}.
 
 ----
 #### Meta-properties
diff --git a/properties/P000063.md b/properties/P000063.md
index 1cbdeaf257..a4b0f5e212 100644
--- a/properties/P000063.md
+++ b/properties/P000063.md
@@ -1,15 +1,22 @@
 ---
 uid: P000063
 name: Čech complete
+aliases:
+  - Topologically complete
 refs:
   - zb: "0684.54001"
     name: General Topology (Engelking, 1989)
+  - zb: "0117.15903"
+    name: A characterization of topologically complete spaces in the sense of E. Čech in terms of convergence of functions. (Frolik, 1963)
 ---
 A {P6} space $X$ that is a $G_\delta$ set in some compactification of $X$ (equivalently, in every compactification of $X$).
 
 Equivalently, there is a sequence $\mathcal{U}_1, \mathcal{U}_2, \dots$ of open covers of $X$ such that whenever $\mathcal{F}$ is a family of closed sets with the finite intersection property and such that for each $n$ there is some $F_n \in \mathcal{F}$ with $F_n \subseteq U$ for some $U \in \mathcal{U}_n$, then $\bigcap \mathcal F \neq \emptyset$.
 
-See Section 3.9 of {{zb:0684.54001}}, specifically Theorems 3.9.1 and 3.9.2 for the equivalences above.
+See Section 3.9 ("Čech-complete spaces") of {{zb:0684.54001}}, specifically Theorems 3.9.1 and 3.9.2 for the equivalences above.
+
+Such spaces are called *topologically complete* in {{zb:0117.15903}};
+this last term has also been used for {P55} and {P221}.
 
 ----
 #### Meta-properties
diff --git a/properties/P000085.md b/properties/P000085.md
index d89d7e236a..13ad2b4191 100644
--- a/properties/P000085.md
+++ b/properties/P000085.md
@@ -2,7 +2,7 @@
 uid: P000085
 name: Basically disconnected
 refs:
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman & Jerison)
 ---
 
@@ -13,7 +13,7 @@ equivalently, the complement of a zero set.
 
 Equivalently, any two disjoint open sets, at least one of which is a cozero set, have disjoint closures.
 
-Defined in problem 1H of {{doi:10.1007/978-1-4615-7819-2}}.
+Defined in problem 1H of {{zb:1380.46022}}.
 
 No additional separation axiom is assumed here.
 
diff --git a/properties/P000162.md b/properties/P000162.md
index 813b9a91f8..5ec4567f0c 100644
--- a/properties/P000162.md
+++ b/properties/P000162.md
@@ -4,7 +4,7 @@ name: Realcompact
 refs:
   - zb: "0684.54001"
     name: General Topology (Engelking, 1989)
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman and Jerison)
   - wikipedia: Ultrafilter
     name: Ultrafilter on Wikipedia
@@ -12,7 +12,7 @@ refs:
 
 A space $X$ that is homeomorphic to a closed subset of $\mathbb{R}^\kappa$ for some cardinal $\kappa$.
 
-Equivalently (see {{doi:10.1007/978-1-4615-7819-2}}), $X$ is {P6} and every real $z$-ultrafilter $\mathcal U$ on the space $X$ is fixed,
+Equivalently (see {{zb:1380.46022}}), $X$ is {P6} and every real $z$-ultrafilter $\mathcal U$ on the space $X$ is fixed,
 that is, $\bigcap\mathcal{U}\neq\emptyset$.
 
 A *$z$-ultrafilter* is an ultrafilter on the lattice of zero-sets of $X$ (see {{wikipedia:Ultrafilter}} for the general definition of an ultrafilter on a poset). A *real $z$-ultrafilter* is a $z$-ultrafilter with countable intersection property, that is, for any countable $\mathcal{F}\subseteq \mathcal{U}$ we have $\bigcap\mathcal{F}\neq \emptyset$.
diff --git a/properties/P000164.md b/properties/P000164.md
index af5a145864..660f996937 100644
--- a/properties/P000164.md
+++ b/properties/P000164.md
@@ -6,7 +6,7 @@ aliases:
 refs:
 - wikipedia: Measurable_cardinal
   name: Measurable cardinal on Wikipedia
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman and Jerison)
 - doi: 10.1007/3-540-44761-X
   name: Set Theory (Jech)
@@ -22,7 +22,7 @@ A cardinal $\kappa$ is called *measurable* if $\kappa$ is uncountable and there
 
 Equivalently, $\kappa$ is uncountable and there exists a free ultrafilter $\mathcal{U}$ on $\kappa$ such that $\mathcal{U}$ is *$\kappa$-complete*, i.e., if $\mathcal{F}\subseteq \mathcal{U}$ and $|\mathcal{F}| < \kappa$ then $\bigcap\mathcal{F}\in \mathcal{U}$. (See {{wikipedia:Measurable_cardinal}} for more details.)
 
-Note: Some authors, for example {{doi:10.1007/978-1-4615-7819-2}}, refer to measurable cardinals as those cardinals $\kappa$ for which there exists a $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ which is non-trivial. If $\kappa$ is the smallest such cardinal, then a non-trivial $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ is $\kappa$-additive (see lemma 10.2 of {{doi:10.1007/3-540-44761-X}} and comments preceding it), so $\kappa$ is also measurable by the above definition.
+Note: Some authors, for example {{zb:1380.46022}}, refer to measurable cardinals as those cardinals $\kappa$ for which there exists a $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ which is non-trivial. If $\kappa$ is the smallest such cardinal, then a non-trivial $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ is $\kappa$-additive (see lemma 10.2 of {{doi:10.1007/3-540-44761-X}} and comments preceding it), so $\kappa$ is also measurable by the above definition.
 
 (The existence of a measurable cardinal cannot be proven in ZFC.
 So spaces whose construction does not depend on set-theoretic axioms beyond ZFC should never have this property marked as false.)
diff --git a/properties/P000207.md b/properties/P000207.md
index ab944d46f9..d6549286d3 100644
--- a/properties/P000207.md
+++ b/properties/P000207.md
@@ -17,6 +17,8 @@ For each neighborhood $U$ of the diagonal $\Delta=\{(x,x)\mid x\in X\}$
 in $X\times X$, there is a neighborhood $V$ of the diagonal such that
 $V\circ V\subseteq U$.
 
+This is equivalent to the family $\mathcal{U}$ of neighborhoods of $\Delta_X$ forming a uniformity, but the topology of $X$ and that of $(X, \mathcal{U})$ do not need to agree. If $X$ is {P12} then both topologies coincide.
+
 In Theorem 2.6 of {{doi:10.2307/1993026}} this property was shown to be equivalent to
 *almost $2$-fully normal*: each open cover $\mathcal U$ has an open almost $2$-star
 refinement $\mathcal V$, that is $\mathcal{V}$ is a refinement of $\mathcal{U}$ and for any $x, y, z$ with $y, z\in \text{St}(x, \mathcal{V})$ there exists $U\in\mathcal{U}$ with $y, z\in U$.
diff --git a/properties/P000215.md b/properties/P000215.md
index 8b8ed9bebc..47d46163f0 100644
--- a/properties/P000215.md
+++ b/properties/P000215.md
@@ -2,13 +2,13 @@
 uid: P000215
 name: Hereditarily realcompact
 refs:
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman & Jerison)
 ---
 
 Every subspace is {P162}. 
 
-Equivalently, $X$ is {P6} and $X\setminus \{x\}$ is realcompact for each $x\in X$. (theorem 8.17 of {{doi:10.1007/978-1-4615-7819-2}})
+Equivalently, $X$ is {P6} and $X\setminus \{x\}$ is realcompact for each $x\in X$. (theorem 8.17 of {{zb:1380.46022}})
 
 ----
 #### Meta-properties
diff --git a/properties/P000221.md b/properties/P000221.md
new file mode 100644
index 0000000000..be383c61fe
--- /dev/null
+++ b/properties/P000221.md
@@ -0,0 +1,44 @@
+---
+uid: P000221
+name: Dieudonné complete
+aliases:
+  - Completely uniformizable
+  - Topologically complete
+refs:
+  - wikipedia: Completely_uniformizable_space
+    name: Completely uniformizable space
+  - zb: "1380.46022"
+    name: Rings of Continuous Functions (Gillman & Jerison)
+  - mr: 370454
+    name: General Topology (Kelley)
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+  - zb: "1052.54001"
+    name: General Topology (Willard, 1970)
+  - zb: "0024.36301"
+    name: Sur les espaces uniformes complets (Dieudonné)
+---
+
+There exists at least one [complete uniformity](https://en.wikipedia.org/wiki/Uniform_space#Completeness)
+that induces the topology of $X$.
+
+This is equivalent to each of the following:
+- $X$ is homeomorphic to a closed subspace of a product of completely pseudometrizable spaces.
+- $X$ is homeomorphic to a closed subspace of a product of {P121} spaces.
+
+For the equivalence, see Problem 8.5.13(z) in {{zb:0684.54001}} and page 285 of {{zb:0024.36301}}.
+
+Terminology:
+We call a 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 a *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$.
+(Compare with the definition of complete uniformity in 15.7 of {{zb:1380.46022}} where uniform structure is defined using pseudometrics.)
+
+Such spaces are called *Dieudonné complete* (Problem 8.5.13 in {{zb:0684.54001}}) or *completely uniformizable* (Problem 39B in {{zb:1052.54001}}).
+They are called *topologically complete* on page 208 of {{mr:370454}}; 
+this last term has also been used for {P55} and {P63}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
+- This property is preserved by arbitrary products.
+- This property is hereditary with respect to closed sets.
diff --git a/spaces/S000074/properties/P000162.md b/spaces/S000074/properties/P000162.md
index e8fb1a46bd..563d3d56c1 100644
--- a/spaces/S000074/properties/P000162.md
+++ b/spaces/S000074/properties/P000162.md
@@ -3,8 +3,8 @@ space: S000074
 property: P000162
 value: true
 refs:
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman and Jerison)
 ---
 
-The identity function $\text{Id}:X\to \mathbb{R}^2$, $\text{Id}(x) = x$ from {S74} to {S176} is a continuous injection. Since every subspace of {S176} is realcompact ({S176} is {P5} and {P131}, and see {T384}), {S74} is realcompact from corollary 8.18 in {{doi:10.1007/978-1-4615-7819-2}}.
+The identity function $\text{Id}:X\to \mathbb{R}^2$, $\text{Id}(x) = x$ from {S74} to {S176} is a continuous injection. Since every subspace of {S176} is realcompact ({S176} is {P5} and {P131}, and see {T384}), {S74} is realcompact from corollary 8.18 in {{zb:1380.46022}}.
diff --git a/spaces/S000107/properties/P000162.md b/spaces/S000107/properties/P000162.md
index 223c11d460..c6ef1b0d2d 100644
--- a/spaces/S000107/properties/P000162.md
+++ b/spaces/S000107/properties/P000162.md
@@ -3,9 +3,9 @@ space: S000107
 property: P000162
 value: true
 refs:
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman and Jerison)
 ---
 
-The identity function $\text{Id}:\mathbb{R}^\omega\to \mathbb{R}^\omega$, $\text{Id}(x) = x$ from {S107} to $\mathbb{R}^\omega$ with product topology is a continuous bijection. Since every subspace of $\mathbb{R}^\omega$ with product topology is realcompact ($\mathbb{R}^\omega$ is {P5} and {P131}, and see {T384}), {S107} is realcompact from corollary 8.18 in {{doi:10.1007/978-1-4615-7819-2}}.
+The identity function $\text{Id}:\mathbb{R}^\omega\to \mathbb{R}^\omega$, $\text{Id}(x) = x$ from {S107} to $\mathbb{R}^\omega$ with product topology is a continuous bijection. Since every subspace of $\mathbb{R}^\omega$ with product topology is realcompact ($\mathbb{R}^\omega$ is {P5} and {P131}, and see {T384}), {S107} is realcompact from corollary 8.18 in {{zb:1380.46022}}.
 
diff --git a/spaces/S000153/properties/P000162.md b/spaces/S000153/properties/P000162.md
index 58cc0fca05..d35ecb5671 100644
--- a/spaces/S000153/properties/P000162.md
+++ b/spaces/S000153/properties/P000162.md
@@ -3,8 +3,8 @@ space: S000153
 property: P000162
 value: false
 refs:
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman and Jerison)
 ---
 
-The subspace $X\subseteq Y$ of {S153} given by $X = \{(x, 0) : 0 < x < \omega_1\}$ is a closed copy of $\omega_1$ in $Y$. If $Y$ were realcompact, then its closed subspace $X$ would be realcompact (see theorem 8.10 in {{doi:10.1007/978-1-4615-7819-2}}). But $\omega_1$ is a pseudocompact non-compact Tychonoff space, so is not realcompact, see {T388}.
+The subspace $X\subseteq Y$ of {S153} given by $X = \{(x, 0) : 0 < x < \omega_1\}$ is a closed copy of $\omega_1$ in $Y$. If $Y$ were realcompact, then its closed subspace $X$ would be realcompact (see theorem 8.10 in {{zb:1380.46022}}). But $\omega_1$ is a pseudocompact non-compact Tychonoff space, so is not realcompact, see {T388}.
diff --git a/spaces/S000208/README.md b/spaces/S000208/README.md
index 912e13430c..8032cbb16c 100644
--- a/spaces/S000208/README.md
+++ b/spaces/S000208/README.md
@@ -4,7 +4,7 @@ name: Hewitt realcompactification of Rudin's Dowker space
 refs:
   - zb: "0224.54019"
     name: A normal space X for which X×I is not normal (M.E. Rudin)
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman & Jerison)
   - wikipedia: Cofinality#Cofinality_of_ordinals_and_other_well-ordered_sets
     name: Cofinality on Wikipedia
@@ -13,4 +13,4 @@ refs:
 $X$ is the subspace of the product $\prod_{n\in\omega}(\omega_{n+1}+1)$ with the box topology consisting of all $f\in \prod_{n\in \omega}(\omega_{n+1}+1)$ such that $\omega< \text{cf}(f(n))$ for all $n$ (see {{wikipedia:Cofinality#Cofinality_of_ordinals_and_other_well-ordered_sets}}).
 
 Defined (as the space called $X'$) and shown to be the Hewitt realcompactification of {S138} in section IV.4 of {{zb:0224.54019}} 
-(see remark 8.8 of {{doi:10.1007/978-1-4615-7819-2}} for the definition of Hewitt realcompactification).
+(see remark 8.8 of {{zb:1380.46022}} for the definition of Hewitt realcompactification).
diff --git a/spaces/S000216/README.md b/spaces/S000216/README.md
index 87ada22090..fe6a2a565b 100644
--- a/spaces/S000216/README.md
+++ b/spaces/S000216/README.md
@@ -2,7 +2,7 @@
 uid: S000216
 name: Katětov's non-normal subspace of $\beta\mathbb{N}$
 refs:
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman & Jerison)
 ---
 
@@ -10,4 +10,4 @@ Fix a bijection $\varphi:\mathbb{N}\to\mathbb{Q}$. For each irrational $r$ fix a
 
 Katětov's non-normal subspace of $\beta\mathbb{N}$ is the space $X=\mathbb{N}\cup D$ where $D = \{p_E : E\in\mathcal{E}\}$.
 
-Constructed in exercise 6Q of {{doi:10.1007/978-1-4615-7819-2}}.
+Constructed in exercise 6Q of {{zb:1380.46022}}.
diff --git a/theorems/T000382.md b/theorems/T000382.md
index bef4bd18ff..a183dffa13 100644
--- a/theorems/T000382.md
+++ b/theorems/T000382.md
@@ -10,7 +10,7 @@ then:
 refs:
   - doi: 10.1090/S0002-9939-1973-0322812-9  
     name: Certain Subsets of Products of θ-refinable Spaces are Realcompact (P. Zenor)
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman & Jerison)
 ---
 
diff --git a/theorems/T000383.md b/theorems/T000383.md
index 8c3adff918..b2a939122b 100644
--- a/theorems/T000383.md
+++ b/theorems/T000383.md
@@ -5,12 +5,12 @@ if:
 then:
   P000164: true
 refs:
-  - doi: 10.1007/978-1-4615-7819-2
+  - zb: "1380.46022"
     name: Rings of Continuous Functions (Gillman and Jerison)
   - wikipedia: Measurable_cardinal
     name: Measurable cardinal on Wikipedia
 ---
 
-See Theorem 12.5 in {{doi:10.1007/978-1-4615-7819-2}}: in ZFC a measurable cardinal must be strongly inaccessible.
+See Theorem 12.5 in {{zb:1380.46022}}: in ZFC a measurable cardinal must be strongly inaccessible.
 
 Also {{wikipedia:Measurable_cardinal}}.
diff --git a/theorems/T000384.md b/theorems/T000384.md
index 67e0880e0a..82a0a59278 100644
--- a/theorems/T000384.md
+++ b/theorems/T000384.md
@@ -9,10 +9,10 @@ then:
 refs:
 - zb: "0684.54001"
   name: General Topology (Engelking, 1989)
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman and Jerison)
 ---
 
 See Theorem 3.8.2 of {{zb:0684.54001}} (where the {P18} property assumes {P5}).
 
-Also Theorem 8.2 of {{doi:10.1007/978-1-4615-7819-2}} (where all spaces are assumed {P6}).
+Also Theorem 8.2 of {{zb:1380.46022}} (where all spaces are assumed {P6}).
diff --git a/theorems/T000386.md b/theorems/T000386.md
index 2664032d12..bc9546b5d5 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} [(Explore)](https://topology.pi-base.org/spaces?q=pseudocompact+%2B+metrizable+%2B+%7Ecompact). It follows that $X$ is a closed subspace of the {P16} space $\prod_\alpha \pi_\alpha(X)$, and so {P16}.
diff --git a/theorems/T000742.md b/theorems/T000742.md
index 5f125f830d..71020d8140 100644
--- a/theorems/T000742.md
+++ b/theorems/T000742.md
@@ -8,7 +8,7 @@ if:
 then:
   P000215: true
 refs:
-- doi: 10.1007/978-1-4615-7819-2
+- zb: "1380.46022"
   name: Rings of Continuous Functions (Gillman & Jerison)
 ---
 
@@ -17,5 +17,5 @@ Every {P53} space is {P7} and {P194}
 [(Explore)](https://topology.pi-base.org/spaces?q=Metrizable%2B%7ESubmetacompact).
 So every subspace of $Y$ satisfies the hypotheses of {T382},
 and hence is {P162}.
-By Corollary 8.18 of {{doi:10.1007/978-1-4615-7819-2}}
+By Corollary 8.18 of {{zb:1380.46022}}
 every subspace of $X$ is {P162}.
diff --git a/theorems/T000914.md b/theorems/T000914.md
new file mode 100644
index 0000000000..46c416cc59
--- /dev/null
+++ b/theorems/T000914.md
@@ -0,0 +1,9 @@
+---
+uid: T000914
+if:
+  P000221: true
+then:
+  P000012: true
+---
+
+{P12} spaces are precisely the spaces admitting a uniformity.
diff --git a/theorems/T000915.md b/theorems/T000915.md
new file mode 100644
index 0000000000..03e4fd95a4
--- /dev/null
+++ b/theorems/T000915.md
@@ -0,0 +1,13 @@
+---
+uid: T000915
+if:
+  P000162: true
+then:
+  P000221: true
+refs:
+  - zb: "1380.46022"
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+See Corollary 15.14 of {{zb:1380.46022}} 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/T000916.md b/theorems/T000916.md
new file mode 100644
index 0000000000..41971d176d
--- /dev/null
+++ b/theorems/T000916.md
@@ -0,0 +1,16 @@
+---
+uid: T000916
+if:
+  and:
+  - P000001: true
+  - P000164: true
+  - P000221: true
+then:
+  P000162: true
+refs:
+  - zb: "1380.46022"
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+A {P221} {P1} space is {P6} [(Explore)](https://topology.pi-base.org/spaces?q=dieudonne+complete+%2B+T_0+%2B+not+completely+regular).
+Now apply Theorem 15.20 of {{zb:1380.46022}}.
diff --git a/theorems/T000917.md b/theorems/T000917.md
new file mode 100644
index 0000000000..586b66edd0
--- /dev/null
+++ b/theorems/T000917.md
@@ -0,0 +1,19 @@
+---
+uid: T000917
+if:
+  and:
+  - P000134: true
+  - P000030: true
+then:
+  P000221: true
+refs:
+  - zb: "1358.54001"
+    name: General Topology (Kelley)
+---
+
+By taking the Kolmogorov quotient we can assume $X$ is {P3}.
+Assume $X$ is not {P221}. Since $X$ is {P207} [(Explore)](https://topology.pi-base.org/spaces?q=R_1+%2B+paracompact+%2B+not+strongly+collectionwise+normal), the neighbourhoods of the diagonal $\Delta_X\subseteq X\times X$ form a uniformity $\mathcal{U}$ on $X$, and since $X$ is {P12} [(Explore)](https://topology.pi-base.org/spaces?q=R_1+%2B+paracompact+%2B+not+completely+regular), the uniformity is compatible with $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 cluster points (see Theorem 6.21 on page 191 of {{zb:1358.54001}}), 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 on page 156 of {{zb:1358.54001}}, the open cover $\{U_x : x\in X\}$ is even, so there exists $V\in\mathcal{U}$ such that each $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$.