diff --git a/properties/P000162.md b/properties/P000162.md
index 5ec4567f0..608bf549a 100644
--- a/properties/P000162.md
+++ b/properties/P000162.md
@@ -18,3 +18,5 @@ 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$.
 
 See also section 3.11 in {{zb:0684.54001}}.
+
+Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.
diff --git a/properties/P000221.md b/properties/P000221.md
index be383c61f..69d5c6e35 100644
--- a/properties/P000221.md
+++ b/properties/P000221.md
@@ -36,6 +36,8 @@ Such spaces are called *Dieudonné complete* (Problem 8.5.13 in {{zb:0684.54001}
 They are called *topologically complete* on page 208 of {{mr:370454}}; 
 this last term has also been used for {P55} and {P63}.
 
+Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.
+
 ----
 #### Meta-properties
 
diff --git a/theorems/T000923.md b/theorems/T000923.md
new file mode 100644
index 000000000..27b9513e7
--- /dev/null
+++ b/theorems/T000923.md
@@ -0,0 +1,18 @@
+---
+uid: T000923
+if:
+  and:
+  - P000112: true
+  - P000006: true
+then:
+  P000221: true
+refs:
+  - zb: "1380.46022"
+    name: Rings of Continuous Functions (Gillman & Jerison)
+  - zb: "1323.22001"
+    name: Topological groups and related structures (Arhangel’skii, Tkachenko)
+---
+
+See proposition 6.10.8 of {{zb:1323.22001} and exercise 15U.3 of {{zb:1380.46022}}. 
+
+*Remark.* Note that since {P112} is a hereditary property, it follows that the space is hereditarily {P221}. This improves {T742}.