diff --git a/properties/P000243.md b/properties/P000243.md
index 19af65a1c4..975cb6e24d 100644
--- a/properties/P000243.md
+++ b/properties/P000243.md
@@ -20,3 +20,6 @@ Defined on page 14 of {{zb:0559.54003}}.
 #### Meta-properties
 
 - This property is hereditary with respect to dense sets.
+- This property is hereditary with respect to open sets.
+- $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does.
+- This property is preserved by countable products.
diff --git a/properties/P000244.md b/properties/P000244.md
index bf7b1a17cd..bd74083923 100644
--- a/properties/P000244.md
+++ b/properties/P000244.md
@@ -23,3 +23,6 @@ Defined on page 16 of {{zb:0559.54003}}.
 #### Meta-properties
 
 - This property is hereditary with respect to dense sets.
+- This property is hereditary with respect to open sets.
+- $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does.
+- This property is preserved by countable products.
diff --git a/spaces/S000108/properties/P000243.md b/spaces/S000108/properties/P000243.md
new file mode 100644
index 0000000000..44795f072c
--- /dev/null
+++ b/spaces/S000108/properties/P000243.md
@@ -0,0 +1,7 @@
+---
+space: S000108
+property: P000243
+value: true
+---
+
+The set $\{\{n\}: n < \omega\}$ is a countable $\pi$-base for $\beta \omega$.
diff --git a/spaces/S000111/properties/P000243.md b/spaces/S000111/properties/P000243.md
new file mode 100644
index 0000000000..c6a79462b4
--- /dev/null
+++ b/spaces/S000111/properties/P000243.md
@@ -0,0 +1,7 @@
+---
+space: S000111
+property: P000243
+value: true
+---
+
+$X$ is a dense subspace of {S108} and {S108|P243}.
diff --git a/spaces/S000216/properties/P000243.md b/spaces/S000216/properties/P000243.md
new file mode 100644
index 0000000000..9bef40420d
--- /dev/null
+++ b/spaces/S000216/properties/P000243.md
@@ -0,0 +1,7 @@
+---
+space: S000216
+property: P000243
+value: true
+---
+
+$X$ is a dense subspace of {S108} and {S108|P243}.
diff --git a/theorems/T000902.md b/theorems/T000902.md
index d32fd521d4..a16a29f392 100644
--- a/theorems/T000902.md
+++ b/theorems/T000902.md
@@ -1,9 +1,20 @@
 ---
 uid: T000902
 if:
-  P000027: true
+  and:
+  - P000244: true
+  - P000026: true
 then:
   P000243: true
+refs:
+  - zb: "0559.54003"
+    name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology
 ---
 
-A base for the topology is a $\pi$-base.
+Let $A$ be a countable dense subset of $X$.
+For each $x\in A$, let $\mathcal V_x$ be a countable local $\pi$-base for $x$.
+Then $\bigcup\{\mathcal V_x:x\in A\}$ is a countable (global) $\pi$-base.
+
+To see this, if $O$ is a nonempty open set, there is some $x\in A\cap O$. Hence $O$ contains some $V\in\mathcal V_x$.
+
+This is a special case of Theorem 3.8(b) of {{zb:0559.54003}}.
diff --git a/theorems/T000903.md b/theorems/T000903.md
new file mode 100644
index 0000000000..a0b90fbef1
--- /dev/null
+++ b/theorems/T000903.md
@@ -0,0 +1,16 @@
+---
+uid: T000903
+if:
+  and:
+  - P000011: true
+  - P000029: true
+  - P000191: true
+  - P000244: true
+then:
+  P000163: true
+refs:
+  - zb: "0559.54003"
+    name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology
+---
+
+See Corollary 6.4 of {{zb:0559.54003}}.
diff --git a/theorems/T000904.md b/theorems/T000904.md
new file mode 100644
index 0000000000..5a31e69993
--- /dev/null
+++ b/theorems/T000904.md
@@ -0,0 +1,19 @@
+---
+uid: T000904
+if:
+  and:
+  - P000087: true
+  - P000244: true
+then:
+  P000028: true
+---
+
+Because {T347}, it suffices to check the identity element $e$ has a countable local base.
+Let $\mathcal{U}$ be a countable local $\pi$-base around $e$.
+Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}$.
+
+We claim $\mathcal{W}$ is a countable local base around $e$.
+Every element of $\mathcal{W}$ is an open neighbourhood of $e$.
+And if $V$ is a neighbourhood of $e$, there is an open neighbourhood $O$ of $e$ such that $O\cdot O^{-1}\subseteq V$ by continuity of the group operations.
+By hypothesis, $O$ contains some $U \in \mathcal{U}$.
+Then $U \cdot U^{-1} \subseteq V$.
diff --git a/theorems/T000905.md b/theorems/T000905.md
new file mode 100644
index 0000000000..435731b5e9
--- /dev/null
+++ b/theorems/T000905.md
@@ -0,0 +1,16 @@
+---
+uid: T000905
+if:
+  and:
+  - P000134: true
+  - P000016: true
+  - P000081: true
+then:
+  P000244: true
+refs:
+  - zb: "0559.54003"
+    name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology
+---
+
+The result with {P134} replaced by {P3} is a special case of Theorem 7.13 in {{zb:0559.54003}} (which uses "compact" to mean compact Hausdorff).
+The current result is obtained by passing to the Kolmogorov quotient.