pi-base · prabau · Sep 1, 2026
diff --git a/properties/P000105.md b/properties/P000105.md
@@ -6,7 +6,10 @@ refs:
   name: Encyclopedia of general topology (Hart et al)
 ---
 
-Every open cover of the space has a locally countable open refinement.
+Every open cover of $X$ has a locally countable open refinement.
+
+(A collection $\mathscr V$ of subsets of $X$ is *locally countable*
+if each $x\in X$ has a neighborhood meeting at most countably many elements of $\mathscr V$.)
 
 Defined on page 200 of {{zb:1059.54001}}.
 

diff --git a/theorems/T000587.md b/theorems/T000587.md
diff --git a/theorems/T000654.md b/theorems/T000654.md
@@ -6,4 +6,4 @@ then:
   P000105: true
 ---
 
-Immediate from definitions.
+Immediate from the definitions.
diff --git a/theorems/T000655.md b/theorems/T000655.md
@@ -6,4 +6,4 @@ then:
   P000083: true
 ---
 
-Immediate from definitions.
+Immediate from the definitions.