diff --git a/properties/P000245.md b/properties/P000245.md
new file mode 100644
index 000000000..6004eb6c9
--- /dev/null
+++ b/properties/P000245.md
@@ -0,0 +1,16 @@
+---
+uid: P000245
+name: Has finitely many open sets
+---
+
+$X$ has finitely many open sets.
+
+Equivalently, the Kolmogorov quotient of $X$ is finite.
+
+----
+#### Meta-properties
+
+- This property is hereditary.
+- This property is preserved in any coarser topology.
+- $X$ is {P245} iff its Kolmogorov quotient $\text{Kol}(X)$ is {P78}.
+- This property is preserved by finite products.
diff --git a/theorems/T000189.md b/theorems/T000189.md
index 45ab89a2c..2490a9563 100644
--- a/theorems/T000189.md
+++ b/theorems/T000189.md
@@ -3,13 +3,7 @@ uid: T000189
 if:
   P000078: true
 then:
-  P000027: true
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
+  P000245: true
 ---
 
-Space is finite implies the topology is finite, hence countable. Thus the topology itself is a countable basis.
-
-Follows directly
-from the definition on page 7 of {{zb:0386.54001}}.
+Immediate from the definition.
diff --git a/theorems/T000198.md b/theorems/T000198.md
index 765a4a86e..e71e83b17 100644
--- a/theorems/T000198.md
+++ b/theorems/T000198.md
@@ -1,9 +1,9 @@
 ---
 uid: T000198
 if:
-  P000078: true
+  P000245: true
 then:
   P000208: true
 ---
 
-Finite spaces are compact, and finiteness is a hereditary property.
+Immediate from the definitions.
diff --git a/theorems/T000251.md b/theorems/T000251.md
index eeafd7371..f7ea2a8b6 100644
--- a/theorems/T000251.md
+++ b/theorems/T000251.md
@@ -3,10 +3,7 @@ uid: T000251
 if:
   P000129: true
 then:
-  P000016: true
-refs:
-  - mathse: 3844039
-    name: What topological properties are trivially/vacuously satisfied by any indiscrete space?
+  P000245: true
 ---
 
-All open covers are finite to begin with.
+By definition.
diff --git a/theorems/T000450.md b/theorems/T000450.md
index 80d61ee8b..cdddf1368 100644
--- a/theorems/T000450.md
+++ b/theorems/T000450.md
@@ -1,12 +1,9 @@
 ---
 uid: T000450
 if:
-  P000129: true
+  P000245: true
 then:
   P000027: true
-refs:
-  - mathse: 3844039
-    name: What topological properties are trivially/vacuously satisfied by any indiscrete space?
 ---
 
-A space with only finitely many open sets must by definition have a countable basis.
+The topology is finite, hence countable. Thus the topology itself is a countable basis.
diff --git a/theorems/T000658.md b/theorems/T000658.md
index d601a4c6f..c5a86651b 100644
--- a/theorems/T000658.md
+++ b/theorems/T000658.md
@@ -5,7 +5,7 @@ if:
   - P000016: true
   - P000185: true
 then:
-  P000208: true
+  P000245: true
 ---
 
-The ascending chain condition on open sets holds since there are only finitely many open sets.
+The partition generating the topology must be finite due to $X$ being {P16}, so there are only finitely many open sets.
diff --git a/theorems/T000823.md b/theorems/T000823.md
index bc82ceba9..a719c447d 100644
--- a/theorems/T000823.md
+++ b/theorems/T000823.md
@@ -2,11 +2,10 @@
 uid: T000823
 if:
   and:
-  - P000016: true
-  - P000185: true
+    - P000245: true
+    - P000001: true
 then:
-  P000226: true
+  P000078: true
 ---
 
-The partition generating the topology must be finite due to $X$ being {P16}.
-Hence, there can only be finitely many open sets, which trivially implies {P226}.
\ No newline at end of file
+$\text{Kol}(X)$ is finite, and is equal to $X$ since $X$ is {P1}. So $X$ is finite.
diff --git a/theorems/T000825.md b/theorems/T000825.md
index ae671e426..6490824f9 100644
--- a/theorems/T000825.md
+++ b/theorems/T000825.md
@@ -1,7 +1,7 @@
 ---
 uid: T000825
 if:
-  P000078: true
+  P000245: true
 then:
   P000226: true
 ---