diff --git a/properties/P000028.md b/properties/P000028.md
index 5bae15f1c6..1b517f5979 100644
--- a/properties/P000028.md
+++ b/properties/P000028.md
@@ -16,3 +16,4 @@ Defined on page 7 of {{doi:10.1007/978-1-4612-6290-9}}.
 - This property is hereditary.
 - A space that is locally {P28} (every point has a neighborhood with the property)
 has the property.
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/properties/P000118.md b/properties/P000118.md
index f41503d578..043685d5b9 100644
--- a/properties/P000118.md
+++ b/properties/P000118.md
@@ -11,3 +11,8 @@ A space with a $\sigma$-locally finite $k$-network.
 A family $\mathcal N$ of subsets of $X$ is called a *$k$-network* if for every compact set $K$ and open set $U$ in $X$ with $K\subseteq U$, there exists a finite $\mathcal{N}^* \subseteq \mathcal{N}$ with $K \subseteq \bigcup\mathcal{N}^* \subseteq U$.  The family $\mathcal N$ is *$\sigma$-locally finite* if it is a countable union of locally finite families.
 
 See for example Definition 2.1 in {{doi:10.1016/j.topol.2015.05.085}}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/properties/P000132.md b/properties/P000132.md
index 5290f3e9f5..9b3fc7ee59 100644
--- a/properties/P000132.md
+++ b/properties/P000132.md
@@ -18,3 +18,8 @@ Equivalently, a space in which every open set is an $F_\sigma$ set (a countable
 Defined on page 162 of {{doi:10.1007/978-1-4612-6290-9}}.
 
 Note: A $G_\delta$ space is sometimes called a "perfect space" (Exercise 1.5.H(a) in {{zb:0684.54001}}). Not to be be confused with a space that is a "perfect" in the sense of "perfect set" (= a set equal to its derived set = a closed set that is dense-in-itself), that is, a space without isolated point. See the discussion in <https://en.wikipedia.org/wiki/Talk:Perfect_set#Terminology_issue>.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/properties/P000178.md b/properties/P000178.md
index 3c223d81ab..0b00ec98e4 100644
--- a/properties/P000178.md
+++ b/properties/P000178.md
@@ -11,3 +11,8 @@ refs:
 A space that is {P5} and {P118}.
 
 The notion was introduced in {{doi:10.1090/S0002-9939-1971-0276919-3}}.
+
+----
+#### Meta-properties
+
+- The Kolmogorov quotient $\text{Kol}(X)$ is {P178} iff $X$ is {P11} and {P118}.
diff --git a/theorems/T000516.md b/theorems/T000516.md
index cd68d60dec..2ca9ab56d8 100644
--- a/theorems/T000516.md
+++ b/theorems/T000516.md
@@ -2,13 +2,13 @@
 uid: T000516
 if:
   and:
-    - P000179: true
-    - P000028: true
+  - P000178: true
+  - P000028: true
 then:
   P000053: true
 refs:
-- zb: "0148.16701"
-  name: $\aleph_0$-spaces (E. Michael)
+  - doi: 10.1002/mana.19700450103
+    name: A Metrization Theorem (P. O'Meara)
 ---
 
-See result (B) in {{zb:0148.16701}} (<https://www.jstor.org/stable/24901448>).
+Established in theorem 1 of {{doi:10.1002/mana.19700450103}}, see remarks after definition 2.
diff --git a/theorems/T000517.md b/theorems/T000517.md
index aa9a67c328..d825cec6ff 100644
--- a/theorems/T000517.md
+++ b/theorems/T000517.md
@@ -2,13 +2,11 @@
 uid: T000517
 if:
   and:
-    - P000179: true
-    - P000023: true
+  - P000023: true
+  - P000134: true
+  - P000132: true
 then:
-  P000053: true
-refs:
-- zb: "0148.16701"
-  name: $\aleph_0$-spaces (E. Michael)
+  P000028: true
 ---
 
-See result (C) in {{zb:0148.16701}} (<https://www.jstor.org/stable/24901448>).
+Follows from {T503} by taking Kolmogorov quotient.
diff --git a/theorems/T000788.md b/theorems/T000788.md
new file mode 100644
index 0000000000..3f9b4bcefa
--- /dev/null
+++ b/theorems/T000788.md
@@ -0,0 +1,9 @@
+---
+uid: T000788
+if:
+  P000110: true
+then:
+  P000117: true
+---
+
+Let $(\mathcal{U}_n)$ be development for $X$. Since {T730}, there exist a $\sigma$-locally finite closed refinement $\mathcal{V}_n$ of $\mathcal{U}_n$ for each $n$. Then $\mathcal{N} = \bigcup_n \mathcal{V}_n$ is $\sigma$-locally finite, and if $x\in W$ with $W$ open, then there is $n$ with $\text{St}(x, \mathcal{U}_n)\subseteq W$, and so $\text{St}(x, \mathcal{V}_n)\subseteq \text{St}(x, \mathcal{U}_n)\subseteq W$. Since $\mathcal{V}_n$ is a cover, it follows that there is $V\in\mathcal{V}_n$ with $x\in V\subseteq W$. So $\mathcal{N}$ is a $\sigma$-locally finite network.
diff --git a/theorems/T000820.md b/theorems/T000820.md
new file mode 100644
index 0000000000..6c23ea1d33
--- /dev/null
+++ b/theorems/T000820.md
@@ -0,0 +1,12 @@
+---
+uid: T000820
+if:
+  and:
+  - P000011: true
+  - P000028: true
+  - P000118: true
+then:
+  P000121: true
+---
+
+Follows from {T516} by taking Kolmogorov quotient.