diff --git a/properties/P000208.md b/properties/P000208.md
index cf8152070..960676a06 100644
--- a/properties/P000208.md
+++ b/properties/P000208.md
@@ -31,6 +31,8 @@ Compare with {P226}.
 #### Meta-properties
 
 - This property is hereditary.
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
 - This property is preserved by finite products (see Theorem 3 in {{mathse:5118758}}).
 - This property is preserved by finite disjoint unions.
 - This property is preserved in any coarser topology.
+
diff --git a/theorems/T000929.md b/theorems/T000929.md
new file mode 100644
index 000000000..c66dab7b4
--- /dev/null
+++ b/theorems/T000929.md
@@ -0,0 +1,23 @@
+---
+uid: T000929
+if:
+  and:
+  - P000073: true
+  - P000090: true
+then:
+  P000051: true
+---
+
+$X$ is {P1} since {T174}.
+Let $\le$ denote the corresponding specialization order ($x\le y \iff x\in\overline{\{y\}})$).
+Given a point $a\in X$, its smallest neighborhood is ${\uparrow}a:=\{x\in X:x\ge a\}$.
+
+Assume by contradiction that $X$ is not {P51}.
+There is a nonempty set $A\subseteq X$ such that the subspace $A$ has no isolated point;
+hence for each $a\in A$ we have ${\uparrow} a\cap A\supsetneq\{a\}$, that is, there is some $b\in A$ with $a<b$.
+This allows to construct an increasing sequence $x_1<x_2<\cdots$ in $X$.
+
+The set $B:=\{x\in X:x\le x_i \text{ for some }i\}$ is closed in $X$ and is irreducible ({P39})
+(given $x,x'\in B$, their respective neighborhoods ${\uparrow}x$ and ${\uparrow}x'$ intersect).
+But $B$ has no maximum point, i.e., $B$ has no generic point.
+This shows that $X$ is not {P73}.
diff --git a/theorems/T000930.md b/theorems/T000930.md
new file mode 100644
index 000000000..eeac8e4a9
--- /dev/null
+++ b/theorems/T000930.md
@@ -0,0 +1,15 @@
+---
+uid: T000930
+if:
+  and:
+  - P000051: true
+  - P000208: true
+then:
+  P000078: true
+---
+
+Let $\mathcal{C}$ be the collection of finite open subsets of $X$. It is nonempty since $\emptyset \in \mathcal{C}$, so by {P208} it has a maximal element $U$.
+
+By way of contradiction, assume $U \neq X$. Then $X \setminus U$ is a nonempty subspace, so by {P51} it contains a point $p$ isolated in it, i.e. there is an open $V \subseteq X$ with $V \cap (X \setminus U) = \{ p \}$. Then $U \cup V = U \cup \{ p \}$ is open and finite, and it strictly contains $U$, contradicting the maximality of $U$.
+
+Hence $X = U$ is finite.
diff --git a/theorems/T000931.md b/theorems/T000931.md
new file mode 100644
index 000000000..62352a0bd
--- /dev/null
+++ b/theorems/T000931.md
@@ -0,0 +1,14 @@
+---
+uid: T000931
+if:
+  and:
+  - P000192: true
+  - P000090: true
+  - P000208: true
+then:
+  P000245: true
+---
+
+{P73} {P90} {P208} spaces are {P78}
+[(Explore)](https://topology.pi-base.org/spaces?q=Sober%2BAlexandrov%2BNoetherian%2B%7EFinite).
+Therefore, the desired result follows by passing to the Kolmogorov quotient.