diff --git a/properties/P000088.md b/properties/P000088.md
index 926a46dca4..67c5329286 100644
--- a/properties/P000088.md
+++ b/properties/P000088.md
@@ -12,12 +12,18 @@ refs:
     name: General Topology (Engelking, 1989)
   - zb: "0529.54017"
     name: Collectionwise Hausdorff versus collectionwise normal with respect to compact sets (Reed)
+  - doi: 10.1016/S0166-8641(96)00163-0
+    name: Baireness of $C_k(X)$ for locally compact $X$ (Gruenhage & Ma)
 ---
 
-For every discrete family $(F_i)_{i \in I}$  of closed subsets of $X$, there exists a pairwise disjoint family of open sets $(U_i)_{i \in I}$, such that $F_i \subseteq U_i$ for all $i$.
-Here, a *discrete family* is a family of subsets such that each point of $X$ has a neighborhood meeting at most one of the subsets.
+For every discrete family $(F_i)_{i \in I}$  of closed subsets of $X$, there exists a pairwise disjoint family of open sets $(U_i)_{i \in I}$ with $F_i \subseteq U_i$ for all $i$.
 
-Equivalently, for every discrete family $(F_i)_{i \in I}$  of closed subsets of $X$, there exists a discrete family of open sets $(U_i)_{i \in I}$, such that $F_i \subseteq U_i$ for all $i$.
+Equivalently, for every discrete family $(F_i)_{i \in I}$  of closed subsets of $X$, there exists a discrete family of open sets $(U_i)_{i \in I}$ with $F_i \subseteq U_i$ for all $i$.
+
+Terminology:
+- A *discrete family* is a family of subsets such that each point of $X$ has a neighborhood meeting at most one of the subsets.
+- In the first definition, the family of open sets $(U_i)_i$ is sometimes called a *disjoint open expansion* of the family $(F_i)_i$.
+- In the second definition, the family of open sets $(U_i)_i$ is sometimes called a *discrete open expansion* of the family $(F_i)_i$. (See for example {{doi:10.1016/S0166-8641(96)00163-0}}.)
 
 The equivalence between the two definitions is Theorem 5.1.17 of {{zb:0684.54001}}.
 
diff --git a/spaces/S000082/properties/P000021.md b/spaces/S000082/properties/P000021.md
index 179c4a3a60..87d94d20d5 100644
--- a/spaces/S000082/properties/P000021.md
+++ b/spaces/S000082/properties/P000021.md
@@ -8,4 +8,5 @@ refs:
 ---
 
 Every non-empty set has a limit point, since every non-empty subset of
-{S42} has a limit point (e.g. any lesser point).
+{S42} has a limit point
+(e.g. any point smaller than a point in the set).
diff --git a/theorems/T000661.md b/theorems/T000661.md
new file mode 100644
index 0000000000..09663aa965
--- /dev/null
+++ b/theorems/T000661.md
@@ -0,0 +1,20 @@
+---
+uid: T000661
+if:
+  and:
+  - P000197: true
+  - P000013: true
+then:
+  P000088: true
+refs:
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+---
+
+Given a discrete family $(F_i)_{i \in I}$  of nonempty closed sets in $X$,
+take a point $x_i\in F_i$ for each $i$.
+The subspace $\{x_i:i\in I\}$ is discrete,
+hence countable because $X$ is {P197}.
+
+So there are only countably many $F_i$,
+and one can find a disjoint open expansion of $(F_i)_i$ by Theorem 2.1.14 of {{zb:0684.54001}}.
diff --git a/theorems/T000662.md b/theorems/T000662.md
new file mode 100644
index 0000000000..7a0c0c8793
--- /dev/null
+++ b/theorems/T000662.md
@@ -0,0 +1,21 @@
+---
+uid: T000662
+if:
+  and:
+  - P000198: true
+  - P000007: true
+then:
+  P000088: true
+refs:
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+---
+
+Given a discrete family $(F_i)_{i \in I}$  of nonempty closed sets in $X$,
+take a point $x_i\in F_i$ for each $i$.
+Every singleton $\{x_i\}$ is closed and the subspace $Y=\{x_i:i\in I\}$ is discrete.
+Therefore $Y$ is closed and discrete,
+and hence countable because $X$ is {P198}.
+
+So there are only countably many $F_i$,
+and one can find a disjoint open expansion of $(F_i)_i$ by Theorem 2.1.14 of {{zb:0684.54001}}.