diff --git a/properties/P000162.md b/properties/P000162.md
index eb8d6b9961..813b9a91f8 100644
--- a/properties/P000162.md
+++ b/properties/P000162.md
@@ -6,13 +6,15 @@ refs:
     name: General Topology (Engelking, 1989)
   - doi: 10.1007/978-1-4615-7819-2
     name: Rings of Continuous Functions (Gillman and Jerison)
+  - wikipedia: Ultrafilter
+    name: Ultrafilter on Wikipedia
 ---
 
-A space that is homeomorphic to a closed subset of a (not necessarily finite) power of {S25}.
+A space $X$ that is homeomorphic to a closed subset of $\mathbb{R}^\kappa$ for some cardinal $\kappa$.
 
-Equivalently (see {{doi:10.1007/978-1-4615-7819-2}}), every real $z$-ultrafilter $\mathcal U$ on the space $X$ is fixed,
-i.e., we can find $x\in X$ such that $\mathcal U=\{Z\in Z(X):x\in Z\}$.
-Here, $Z(X)$ is the collection of all zero sets of X, a $z$-ultrafilter is an ultrafilter on the lattice $Z(X)$, and
-it is real when it is closed under countable intersections.
+Equivalently (see {{doi:10.1007/978-1-4615-7819-2}}), $X$ is {P6} and every real $z$-ultrafilter $\mathcal U$ on the space $X$ is fixed,
+that is, $\bigcap\mathcal{U}\neq\emptyset$.
+
+A *$z$-ultrafilter* is an ultrafilter on the lattice of zero-sets of $X$ (see {{wikipedia:Ultrafilter}} for the general definition of an ultrafilter on a poset). A *real $z$-ultrafilter* is a $z$-ultrafilter with countable intersection property, that is, for any countable $\mathcal{F}\subseteq \mathcal{U}$ we have $\bigcap\mathcal{F}\neq \emptyset$.
 
 See also section 3.11 in {{zb:0684.54001}}.
diff --git a/properties/P000164.md b/properties/P000164.md
index a9677bba90..ce397ae934 100644
--- a/properties/P000164.md
+++ b/properties/P000164.md
@@ -1,14 +1,28 @@
 ---
 uid: P000164
-name: Non-measurable cardinality
+name: Cardinality less than every measurable cardinal
+aliases:
+  - Non-measurable cardinality
 refs:
 - wikipedia: Measurable_cardinal
   name: Measurable cardinal on Wikipedia
 - doi: 10.1007/978-1-4615-7819-2
   name: Rings of Continuous Functions (Gillman and Jerison)
+- doi: 10.1007/3-540-44761-X
+  name: Set Theory (Jech)
 ---
 
-The cardinality of the space is not a measurable cardinal ({{wikipedia:Measurable_cardinal}}).
+The cardinality of the space is smaller than every measurable cardinal, if one exists.
 
-(Note that the existence of a measurable cardinal cannot be proven in ZFC, so no space should ever have this
-property marked as false. See {T383}.)
+A cardinal $\kappa$ is called *measurable* if $\kappa$ is uncountable and there exists a measure $\mu:2^\kappa\to \{0, 1\}$ such that 
+
+1. $\mu$ is *$\kappa$-additive*: $\mu(\bigcup_{i\in I} A_i) = \sum_{i\in I} \mu(A_i)$ for any family $(A_i)_{i\in I}\subseteq 2^\kappa$ of pairwise disjoint sets with $|I| < \kappa$,
+
+2. $\mu$ is non-trivial: $\mu(\kappa) = 1$ and $\mu(\{x\}) = 0$ for all $x\in \kappa$. 
+
+Equivalently, $\kappa$ is uncountable and there exists a free ultrafilter $\mathcal{U}$ on $\kappa$ such that $\mathcal{U}$ is *$\kappa$-complete*, i.e., if $\mathcal{F}\subseteq \mathcal{U}$ and $|\mathcal{F}| < \kappa$ then $\bigcap\mathcal{F}\in \mathcal{U}$. (See {{wikipedia:Measurable_cardinal}} for more details.)
+
+Note: Some authors, for example {{doi:10.1007/978-1-4615-7819-2}}, refer to measurable cardinals as those cardinals $\kappa$ for which there exists a $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ which is non-trivial. If $\kappa$ is the smallest such cardinal, then a non-trivial $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ is $\kappa$-additive (see lemma 10.2 of {{doi:10.1007/3-540-44761-X}} and comments preceeding it), so $\kappa$ is also measurable by the above definition.
+
+(The existence of a measurable cardinal cannot be proven in ZFC.
+So spaces whose construction does not depend on set-theoretic axioms beyond ZFC should never have this property marked as false.)
diff --git a/spaces/S000007/properties/P000089.md b/spaces/S000007/properties/P000089.md
deleted file mode 100644
index d9be9c57af..0000000000
--- a/spaces/S000007/properties/P000089.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000007
-property: P000089
-value: true
----
-
-Let $f:X \rightarrow X$ be a continuous selfmap and $p \in X$ be the included point.
-If $f$ is a constant function then it has a fixed point.
-Otherwise, it must be that $f(p) = p$, as if were not, then $X\setminus {f(p)}$ would be open
-yet $f^{-1}(X\setminus {f(p)}) \not\ni p$ would not be, making $f$ not continuous.
diff --git a/spaces/S000010/properties/P000089.md b/spaces/S000010/properties/P000089.md
deleted file mode 100644
index 04d1148e82..0000000000
--- a/spaces/S000010/properties/P000089.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000010
-property: P000089
-value: true
----
-
-The only selfmap with no fixed points is given by $0\mapsto 1, 1\mapsto 0$, which is not continuous.
diff --git a/spaces/S000014/properties/P000126.md b/spaces/S000014/properties/P000126.md
deleted file mode 100644
index 6351759014..0000000000
--- a/spaces/S000014/properties/P000126.md
+++ /dev/null
@@ -1,8 +0,0 @@
----
-space: S000014
-property: P000126
-value: true
----
-
-For every $A\subseteq X$, either $0\not\in A$ and $A$ is open,
-or $0\not\in X\setminus A$ and $X\setminus A$ is open (so $A$ is closed).
diff --git a/spaces/S000017/README.md b/spaces/S000017/README.md
index 695a3f32e2..9c0d542d88 100644
--- a/spaces/S000017/README.md
+++ b/spaces/S000017/README.md
@@ -11,7 +11,7 @@ refs:
   - wikipedia: Cocountable_topology
     name: Cocountable topology on Wikipedia
 ---
-Let $X=\mathbb R$ be the set of real numbers.  Define the open sets on $X$ by a letting a set $U \subset X$ be open iff its complement is countable.  Taking the collection of all such sets, $U$, together with both the $\emptyset$ and $X$ yields a topology on $X$.
+Let $X=\mathbb R$ be the set of real numbers.  Define the topology on $X$ by letting a set in $X$ be open iff it is empty or its complement is countable. 
 
 Defined as counterexample #20 ("Countable Complement Topology")
 in {{doi:10.1007/978-1-4612-6290-9}}.
diff --git a/spaces/S000017/properties/P000071.md b/spaces/S000017/properties/P000071.md
new file mode 100644
index 0000000000..f7134afeb8
--- /dev/null
+++ b/spaces/S000017/properties/P000071.md
@@ -0,0 +1,9 @@
+---
+space: S000017
+property: P000071
+value: false
+---
+
+Suppose $A\subseteq X$ is infinite and let $(x_n)\subseteq A$ be a sequence of distinct elements of $A$. If $U_n = X\setminus \{x_m : m\geq n\}$ then the sequence $(U_n)$ is increasing, consists of open sets, and $\bigcup_n U_n = X$. If $A$ were relatively compact then there would be $n$ for which $A\subseteq U_n$. But $x_n\in A\setminus U_n$ so that's impossible.
+
+Since relatively compact subsets of $X$ are finite, if $X$ were {P71} it would be countable. But {S17|P65}.
diff --git a/spaces/S000017/properties/P000126.md b/spaces/S000017/properties/P000126.md
new file mode 100644
index 0000000000..f2a7a28e4b
--- /dev/null
+++ b/spaces/S000017/properties/P000126.md
@@ -0,0 +1,7 @@
+---
+space: S000017
+property: P000126
+value: false
+---
+
+$[0, \infty)$ is neither closed nor open in $X$.
diff --git a/spaces/S000017/properties/P000172.md b/spaces/S000017/properties/P000172.md
new file mode 100644
index 0000000000..0d5f13dff4
--- /dev/null
+++ b/spaces/S000017/properties/P000172.md
@@ -0,0 +1,7 @@
+---
+space: S000017
+property: P000172
+value: true
+---
+
+If $p\in\overline{A}$ and $A$ is countable, then $p\in A$ so one can take a constant sequence. If $A$ is uncountable, pick any sequence $(x_\lambda)_{\lambda < \omega_1}$ of distinct points such that $x_\lambda\in A$. If $U$ is any neighourhood of $p$, then $x_\lambda\notin U$ for at most countably many $\lambda$. If $\beta$ is supremum of those $\lambda$, then $\beta < \omega_1$ since $\text{cf}(\omega_1) = \omega_1$, and so $x_\lambda\in U$ for $\lambda > \beta$. It follows that $(x_\lambda)_{\lambda < \omega_1}$ converges to $p$.
diff --git a/spaces/S000017/properties/P000189.md b/spaces/S000017/properties/P000189.md
new file mode 100644
index 0000000000..df74f034b4
--- /dev/null
+++ b/spaces/S000017/properties/P000189.md
@@ -0,0 +1,7 @@
+---
+space: S000017
+property: P000189
+value: true
+---
+
+Since closed subsets properly contained in $X$ are countable, if $X$ were not $\sigma$-connected then it would be a countable union of countable sets, and so countable. But {S17|P65}.
diff --git a/spaces/S000018/properties/P000071.md b/spaces/S000018/properties/P000071.md
new file mode 100644
index 0000000000..a29fd8951d
--- /dev/null
+++ b/spaces/S000018/properties/P000071.md
@@ -0,0 +1,7 @@
+---
+space: S000018
+property: P000071
+value: false
+---
+
+The Kolmogorov quotient of {S18} is {S17} and {S17|P71}.
diff --git a/spaces/S000018/properties/P000147.md b/spaces/S000018/properties/P000147.md
new file mode 100644
index 0000000000..c2e076199e
--- /dev/null
+++ b/spaces/S000018/properties/P000147.md
@@ -0,0 +1,7 @@
+---
+space: S000018
+property: P000147
+value: true
+---
+
+The Kolmogorov quotient of {S18} is {S17} and {S17|P147}.
diff --git a/spaces/S000018/properties/P000189.md b/spaces/S000018/properties/P000189.md
new file mode 100644
index 0000000000..168ccff348
--- /dev/null
+++ b/spaces/S000018/properties/P000189.md
@@ -0,0 +1,7 @@
+---
+space: S000018
+property: P000189
+value: true
+---
+
+The Kolmogorov quotient of {S18} is {S17} and {S17|P189}.
diff --git a/spaces/S000018/properties/P000206.md b/spaces/S000018/properties/P000206.md
new file mode 100644
index 0000000000..3bc352646c
--- /dev/null
+++ b/spaces/S000018/properties/P000206.md
@@ -0,0 +1,7 @@
+---
+space: S000018
+property: P000206
+value: true
+---
+
+The Kolmogorov quotient of {S18} is {S17} and {S17|P206}.
diff --git a/spaces/S000048/properties/P000001.md b/spaces/S000048/properties/P000001.md
index ac7d6cc369..7db8e427af 100644
--- a/spaces/S000048/properties/P000001.md
+++ b/spaces/S000048/properties/P000001.md
@@ -2,11 +2,6 @@
 space: S000048
 property: P000001
 value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
 ---
 
-If $P,Q \in X$ are distinct, in if $P = (p)$ and $Q = (q)$. Then, without loss of generality, there is some integer $r$ dividing $p$ but not $q$. Thus $P \notin V_r$ but $Q \in V_r$.
-
-See item #3 for space #56 in {{doi:10.1007/978-1-4612-6290-9_6}}.
+By inspection.
diff --git a/spaces/S000048/properties/P000013.md b/spaces/S000048/properties/P000013.md
index 369359978d..0bcc0ed60c 100644
--- a/spaces/S000048/properties/P000013.md
+++ b/spaces/S000048/properties/P000013.md
@@ -2,11 +2,6 @@
 space: S000048
 property: P000013
 value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
 ---
 
-The ideals $(2)$ and $(3)$ are disjoint closed sets but there are no disjoint open sets in $X$.
-
-See item #3 for space #56 in {{doi:10.1007/978-1-4612-6290-9_6}}.
+$\{0\}$ and $\{1\}$ are disjoint closed sets but there are no nonempty disjoint open sets in $X$.
diff --git a/spaces/S000048/properties/P000027.md b/spaces/S000048/properties/P000027.md
index 6c25bab502..b221e12bcc 100644
--- a/spaces/S000048/properties/P000027.md
+++ b/spaces/S000048/properties/P000027.md
@@ -2,11 +2,6 @@
 space: S000048
 property: P000027
 value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
 ---
 
-The sets $V_x$ for $x \in \mathbb{Z}^+$ form a countable basis for $X$.
-
-See item #4 for space #56 in {{doi:10.1007/978-1-4612-6290-9_6}}.
+By construction, it is easy to see that there are only countably many open sets.
diff --git a/spaces/S000048/properties/P000042.md b/spaces/S000048/properties/P000042.md
index 910fefdb1b..6d3b5e2888 100644
--- a/spaces/S000048/properties/P000042.md
+++ b/spaces/S000048/properties/P000042.md
@@ -2,9 +2,7 @@
 space: S000048
 property: P000042
 value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
 ---
 
-See item #5 for space #56 in {{doi:10.1007/978-1-4612-6290-9_6}}.
+Every nonempty open subset of $X$ has a generic point, namely $p$. And {P201} implies
+{P37} [(Explore)](https://topology.pi-base.org/spaces?q=Has+a+generic+point+%2B+not+Path+connected).
diff --git a/spaces/S000048/properties/P000044.md b/spaces/S000048/properties/P000044.md
index fcbff5e100..3c2d2abcbc 100644
--- a/spaces/S000048/properties/P000044.md
+++ b/spaces/S000048/properties/P000044.md
@@ -2,10 +2,6 @@
 space: S000048
 property: P000044
 value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
 ---
 
-Asserted in the General Reference Chart for space #56 in
-{{doi:10.1007/978-1-4612-6290-9_6}}.
+$\{0,p\}$ and $\omega\setminus\{0\}$ form a partition of $X$ into two connected subspaces, each with at least two points.
diff --git a/spaces/S000048/properties/P000051.md b/spaces/S000048/properties/P000051.md
deleted file mode 100644
index 39fa42a6c8..0000000000
--- a/spaces/S000048/properties/P000051.md
+++ /dev/null
@@ -1,11 +0,0 @@
----
-space: S000048
-property: P000051
-value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-Asserted in the General Reference Chart for space #56 in
-{{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000048/properties/P000056.md b/spaces/S000048/properties/P000056.md
deleted file mode 100644
index 101d570584..0000000000
--- a/spaces/S000048/properties/P000056.md
+++ /dev/null
@@ -1,11 +0,0 @@
----
-space: S000048
-property: P000056
-value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-Asserted in the General Reference Chart for space #56 in
-{{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000048/properties/P000057.md b/spaces/S000048/properties/P000057.md
deleted file mode 100644
index 3626b7dbad..0000000000
--- a/spaces/S000048/properties/P000057.md
+++ /dev/null
@@ -1,13 +0,0 @@
----
-space: S000048
-property: P000057
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-$\mathbb{Z}$ is a principal ideal domain and so each prime ideal is generated by a unique prime number. Thus there are countably many prime ideals in $\mathbb{Z}$.
-
-Asserted in the General Reference Chart for space #56 in
-{{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000048/properties/P000129.md b/spaces/S000048/properties/P000129.md
deleted file mode 100644
index 6fb7e41de9..0000000000
--- a/spaces/S000048/properties/P000129.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000048
-property: P000129
-value: false
----
-
-The space is non-trivial by definition.
diff --git a/spaces/S000048/properties/P000138.md b/spaces/S000048/properties/P000138.md
new file mode 100644
index 0000000000..4be94d7579
--- /dev/null
+++ b/spaces/S000048/properties/P000138.md
@@ -0,0 +1,7 @@
+---
+space: S000048
+property: P000138
+value: false
+---
+
+Any $f: X \to X$ s.t. $f(p) = p$ and restricts to a permutation of $\omega$ is easily seen to be continuous. Since there are continuum many permutations of $\omega$, $X$ has at least continuum many self-maps.
diff --git a/spaces/S000048/properties/P000181.md b/spaces/S000048/properties/P000181.md
new file mode 100644
index 0000000000..c9abe18e42
--- /dev/null
+++ b/spaces/S000048/properties/P000181.md
@@ -0,0 +1,7 @@
+---
+space: S000048
+property: P000181
+value: true
+---
+
+By definition.
diff --git a/spaces/S000048/properties/P000192.md b/spaces/S000048/properties/P000192.md
new file mode 100644
index 0000000000..e85559dbd2
--- /dev/null
+++ b/spaces/S000048/properties/P000192.md
@@ -0,0 +1,9 @@
+---
+space: S000048
+property: P000192
+value: true
+---
+
+A nonempty closed subset $A \subset X$, by definition, is either the entirety of $X$, which has $p$ as a generic point; or is a
+nonempty finite subset of $\omega$. In the latter case, $A$ has discrete topology, so it is {P39} iff it is a
+singleton, which, of course, has a generic point as well.
diff --git a/spaces/S000050/README.md b/spaces/S000050/README.md
new file mode 100644
index 0000000000..c7f0f4118c
--- /dev/null
+++ b/spaces/S000050/README.md
@@ -0,0 +1,10 @@
+---
+uid: S000050
+name: Rationals extended by a focal point
+aliases:
+  - Non-Hausdorff cone over the rationals
+  - Open extension of the rationals
+---
+
+Let $X = \mathbb{Q} \cup \{\infty\}$, where $\mathbb{Q}$ has the usual topology on {S27} and is an open subset
+of $X$, and where the only neighborhood of $\infty$ is $X$. See {P202}.
diff --git a/spaces/S000050/properties/P000010.md b/spaces/S000050/properties/P000010.md
new file mode 100644
index 0000000000..c76171782d
--- /dev/null
+++ b/spaces/S000050/properties/P000010.md
@@ -0,0 +1,8 @@
+---
+space: S000050
+property: P000010
+value: true
+---
+
+It is easy to check any regular open $U \subsetneq \mathbb{Q}$ is still regular open in $X$. And, of course, $X$ is regular open in itself. The result now easily follows from {S27|P10} and
+{S27|P202}.
diff --git a/spaces/S000050/properties/P000014.md b/spaces/S000050/properties/P000014.md
new file mode 100644
index 0000000000..6ff1112edc
--- /dev/null
+++ b/spaces/S000050/properties/P000014.md
@@ -0,0 +1,10 @@
+---
+space: S000050
+property: P000014
+value: true
+---
+
+Note that as {S50|P202}, it is
+{P13} [(Explore)](https://topology.pi-base.org/spaces?q=Has+a+point+with+a+unique+neighborhood+%2B+not+Normal).
+Now, any open subset of $X$ is either $X$ itself, which is normal; or an open subset of $\mathbb{Q}$, which is normal
+since {S27|P14}.
diff --git a/spaces/S000050/properties/P000027.md b/spaces/S000050/properties/P000027.md
new file mode 100644
index 0000000000..4401163d2a
--- /dev/null
+++ b/spaces/S000050/properties/P000027.md
@@ -0,0 +1,7 @@
+---
+space: S000050
+property: P000027
+value: true
+---
+
+{S27|P27} and any open basis of {S27} together with $X$ forms an open basis of $X$.
diff --git a/spaces/S000050/properties/P000041.md b/spaces/S000050/properties/P000041.md
new file mode 100644
index 0000000000..f203d51021
--- /dev/null
+++ b/spaces/S000050/properties/P000041.md
@@ -0,0 +1,8 @@
+---
+space: S000050
+property: P000041
+value: false
+---
+
+Being {P41} passes to open subspaces. {S27} is an open subspace of $X$ and
+{S27|P41}.
diff --git a/spaces/S000050/properties/P000045.md b/spaces/S000050/properties/P000045.md
new file mode 100644
index 0000000000..55bd911684
--- /dev/null
+++ b/spaces/S000050/properties/P000045.md
@@ -0,0 +1,9 @@
+---
+space: S000050
+property: P000045
+value: true
+---
+
+Since {S50|P202}, it is
+{P36} [(Explore)](https://topology.pi-base.org/spaces?q=Has+a+point+with+a+unique+neighborhood+%2B+not+Connected).
+And, $X\setminus\{\infty\}$ is {S27}. {S27|P47}.
diff --git a/spaces/S000050/properties/P000056.md b/spaces/S000050/properties/P000056.md
new file mode 100644
index 0000000000..d8ea0c414e
--- /dev/null
+++ b/spaces/S000050/properties/P000056.md
@@ -0,0 +1,7 @@
+---
+space: S000050
+property: P000056
+value: true
+---
+
+It is easy to see that $\{q,\infty\}$ is nowhere dense for all $q \in \mathbb{Q}$, and $X$ is the countable union of all such sets.
diff --git a/spaces/S000050/properties/P000130.md b/spaces/S000050/properties/P000130.md
new file mode 100644
index 0000000000..b285640dd9
--- /dev/null
+++ b/spaces/S000050/properties/P000130.md
@@ -0,0 +1,8 @@
+---
+space: S000050
+property: P000130
+value: false
+---
+
+Being {P130} passes to open subspaces. {S27} is an open subspace of $X$ and
+{S27|P130}.
diff --git a/spaces/S000050/properties/P000181.md b/spaces/S000050/properties/P000181.md
new file mode 100644
index 0000000000..d5709c4825
--- /dev/null
+++ b/spaces/S000050/properties/P000181.md
@@ -0,0 +1,7 @@
+---
+space: S000050
+property: P000181
+value: true
+---
+
+By construction.
diff --git a/spaces/S000050/properties/P000192.md b/spaces/S000050/properties/P000192.md
new file mode 100644
index 0000000000..2cfa186c6c
--- /dev/null
+++ b/spaces/S000050/properties/P000192.md
@@ -0,0 +1,10 @@
+---
+space: S000050
+property: P000192
+value: true
+---
+
+Any nonempty closed subset $A$ of $X$ has to contain $\infty$. If $A = \{\infty\}$, then $A$ clearly has a generic point. Otherwise,
+assume $\{\infty\} \subsetneq A$ and $A$ is {P39}. We see that $A$ cannot contain more than one point of
+$\mathbb{Q}$, as {S27|P3} and $\mathbb{Q}$ is open in $X$. Thus, $A = \{q,\infty\}$ for some
+$q \in \mathbb{Q}$, and $q$ is a generic point of $A$.
diff --git a/spaces/S000050/properties/P000202.md b/spaces/S000050/properties/P000202.md
new file mode 100644
index 0000000000..813297605b
--- /dev/null
+++ b/spaces/S000050/properties/P000202.md
@@ -0,0 +1,7 @@
+---
+space: S000050
+property: P000202
+value: true
+---
+
+By definition, the only neighborhood of $\infty$ is $X$.
diff --git a/spaces/S000086/properties/P000198.md b/spaces/S000086/properties/P000198.md
new file mode 100644
index 0000000000..05dc4448f8
--- /dev/null
+++ b/spaces/S000086/properties/P000198.md
@@ -0,0 +1,7 @@
+---
+space: S000086
+property: P000198
+value: false
+---
+
+The subspace $\mathbb{R}{\times}\{1\}$ is closed uncountable and discrete.
diff --git a/spaces/S000110/properties/P000018.md b/spaces/S000110/properties/P000018.md
deleted file mode 100644
index 51f118c949..0000000000
--- a/spaces/S000110/properties/P000018.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000110
-property: P000018
-value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-See item #5 for space #113 in {{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000110/properties/P000021.md b/spaces/S000110/properties/P000021.md
deleted file mode 100644
index e8e74c7b39..0000000000
--- a/spaces/S000110/properties/P000021.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000110
-property: P000021
-value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-See item #4 for space #113 in {{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000110/properties/P000028.md b/spaces/S000110/properties/P000028.md
deleted file mode 100644
index d0ad4674ad..0000000000
--- a/spaces/S000110/properties/P000028.md
+++ /dev/null
@@ -1,11 +0,0 @@
----
-space: S000110
-property: P000028
-value: false
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-Asserted in the General Reference Chart for space #113 in
-{{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000110/properties/P000059.md b/spaces/S000110/properties/P000059.md
deleted file mode 100644
index 252d37f7e7..0000000000
--- a/spaces/S000110/properties/P000059.md
+++ /dev/null
@@ -1,13 +0,0 @@
----
-space: S000110
-property: P000059
-value: true
-refs:
-- doi: 10.1007/978-1-4612-6290-9_6
-  name: Counterexamples in Topology
----
-
-{S110} is equinumerous with {S108}, which is of size $2^\mathfrak{c}$.
-
-Asserted in the General Reference Chart for space #113 in
-{{doi:10.1007/978-1-4612-6290-9_6}}.
diff --git a/spaces/S000110/properties/P000093.md b/spaces/S000110/properties/P000093.md
new file mode 100644
index 0000000000..42ca3d5627
--- /dev/null
+++ b/spaces/S000110/properties/P000093.md
@@ -0,0 +1,7 @@
+---
+space: S000110
+property: P000093
+value: true
+---
+
+Every $n \in \omega$ has $\{n\}$ as a countable neighborhood and every $F \in M$ has $\omega \cup \{F\}$ as a countable neighborhood.
diff --git a/spaces/S000110/properties/P000132.md b/spaces/S000110/properties/P000132.md
new file mode 100644
index 0000000000..8e82d8617b
--- /dev/null
+++ b/spaces/S000110/properties/P000132.md
@@ -0,0 +1,9 @@
+---
+space: S000110
+property: P000132
+value: true
+---
+
+By construction, every subset of $M$ is closed in $X$. And so is each of the countably many singletons $\{n\}$ for
+$n \in \omega$ since {S110|P2}. Thus, every subset of $X$ is $F_\sigma$, and so every
+subset of $X$ is $G_\delta$ as well.
diff --git a/spaces/S000110/properties/P000147.md b/spaces/S000110/properties/P000147.md
deleted file mode 100644
index 449ce503a9..0000000000
--- a/spaces/S000110/properties/P000147.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000110
-property: P000147
-value: false
-refs:
-- mathse: 4744376
-  name: Are all Hausdorff extremally disconnected P-spaces also regular?
----
-
-Let $\mathcal{U}$ be a free ultrafilter on $\omega$.  Since the ultrafilter is free, for each $n\in\omega$ there exists $A_n\in\mathcal{U}$ not containing $n$.  The intersection of all the $A_n$ is empty.  Then $\bigcap_{n\in\omega} (A_n\cup \{\mathcal{U}\}) = \{\mathcal{U}\}$ is a countable intersection of open sets, but is not open.
diff --git a/spaces/S000110/properties/P000198.md b/spaces/S000110/properties/P000198.md
new file mode 100644
index 0000000000..88b15ad805
--- /dev/null
+++ b/spaces/S000110/properties/P000198.md
@@ -0,0 +1,7 @@
+---
+space: S000110
+property: P000198
+value: false
+---
+
+By construction, $M$ is a closed discrete subspace of $X$. There are $2^\mathfrak{c}$ free ultrafilters on $\omega$, i.e., $|M| = 2^\mathfrak{c}$.
diff --git a/spaces/S000136/properties/P000164.md b/spaces/S000136/properties/P000164.md
index 9de9348d22..27fdddb5f0 100644
--- a/spaces/S000136/properties/P000164.md
+++ b/spaces/S000136/properties/P000164.md
@@ -4,4 +4,4 @@ property: P000164
 value: true
 ---
 
-$|X| = 2^{2^\mathfrak{c}}$ is non-measurable
\ No newline at end of file
+$|X| = 2^{2^\mathfrak{c}}$ is smaller than every measurable cardinal.
\ No newline at end of file
diff --git a/spaces/S000138/properties/P000164.md b/spaces/S000138/properties/P000164.md
index 9f702442c1..d807c3ecd6 100644
--- a/spaces/S000138/properties/P000164.md
+++ b/spaces/S000138/properties/P000164.md
@@ -4,4 +4,4 @@ property: P000164
 value: true
 ---
 
-$X$ has cardinality bounded above by $\aleph_\omega^\omega$, which is below the first inaccessible cardinal and thus $|X|$ is non-measurable.
+$|X| \leq \aleph_\omega^\omega$ and $\aleph_\omega^\omega$ is smaller than every measurable cardinal.
diff --git a/spaces/S000142/README.md b/spaces/S000142/README.md
index 51b3270af3..174a012efe 100644
--- a/spaces/S000142/README.md
+++ b/spaces/S000142/README.md
@@ -8,6 +8,12 @@ refs:
     name: General Topology (Engelking, 1989)
 ---
 
-The subspace $X$ of {S30} $\ell^2$ consisting of those sequences $x=(x_i)_i$ with all $x_i\in\mathbb Q$.
+The subspace $X$ of $\ell^2$ consisting of those sequences $x=(x_i)_i$ with all $x_i\in\mathbb Q$.
+
+The space $\ell^2$ is the Banach space of sequences of real numbers $x=(x_i)_i$ with $\Sigma_i x_i^2<\infty$,
+equipped with the norm $\|x\|_2=(\Sigma_i x_i^2)^{1/2}$ and corresponding distance and topology.
+
+The space $\ell^2$ is topologically homeomorphic to {S30};
+but note the space $X$ is *not* homeomorphic to the subspace $\mathbb Q^\omega$ of $\mathbb R^\omega$.
 
 See {{mathse:151954}} or Example 6.2.19 in {{zb:0684.54001}}.
diff --git a/spaces/S000144/properties/P000089.md b/spaces/S000144/properties/P000089.md
deleted file mode 100644
index fca384fe8a..0000000000
--- a/spaces/S000144/properties/P000089.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000144
-property: P000089
-value: true
----
-
-Note that in $X$, $x \leq y$ iff $x \in \overline{\{y\}}$, i.e., $\leq$ corresponds to the specialization preorder, which is preserved by continuous functions. Let $f: X\to X$ be continuous. Then $x \leq y$ implies $f(x) \leq f(y)$. Hence, if neither $0$ nor $1$ are fixed points, the range of $f$ must be $\{a\}$ or $\{b\}$, making either $a$ or $b$ a fixed point.
diff --git a/spaces/S000152/README.md b/spaces/S000152/README.md
new file mode 100644
index 0000000000..7d182989ee
--- /dev/null
+++ b/spaces/S000152/README.md
@@ -0,0 +1,17 @@
+---
+uid: S000152
+name: Poset $\{-1,0_a,0_b\}\cup\{1/n\}_{n=1}^\infty$ with Alexandrov topology
+refs:
+  - wikipedia: Alexandrov_topology
+    name: Alexandrov topology on Wikipedia
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?"
+---
+
+Consider the set $\{1/n\}_{n=1}^\infty$ with its usual order. Let,
+
+$\quad X=\{-1,0_a,0_b\}\cup\{1/n\}_{n=1}^\infty$
+
+where either of the zeros is smaller than all $1/n$, the two zeros are incomparable, and $-1$ is smaller than everything else. Then equip $X$ with the Alexandrov topology associated to the partial order defined above; that is, the open sets are the upper sets for $\le$.
+
+This space is described in part 2 of {{mathse:5007860}}.
diff --git a/spaces/S000152/properties/P000039.md b/spaces/S000152/properties/P000039.md
new file mode 100644
index 0000000000..62e1db7f1e
--- /dev/null
+++ b/spaces/S000152/properties/P000039.md
@@ -0,0 +1,10 @@
+---
+space: S000152
+property: P000039
+value: true
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?"
+---
+
+See part 2 of {{mathse:5007860}}.
diff --git a/spaces/S000152/properties/P000073.md b/spaces/S000152/properties/P000073.md
new file mode 100644
index 0000000000..fe405e42ee
--- /dev/null
+++ b/spaces/S000152/properties/P000073.md
@@ -0,0 +1,10 @@
+---
+space: S000152
+property: P000073
+value: true
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?"
+---
+
+See part 2 of {{mathse:5007860}}.
diff --git a/spaces/S000152/properties/P000075.md b/spaces/S000152/properties/P000075.md
new file mode 100644
index 0000000000..f61934eae4
--- /dev/null
+++ b/spaces/S000152/properties/P000075.md
@@ -0,0 +1,10 @@
+---
+space: S000152
+property: P000075
+value: false
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?"
+---
+
+See part 2 of {{mathse:5007860}}.
diff --git a/spaces/S000152/properties/P000090.md b/spaces/S000152/properties/P000090.md
new file mode 100644
index 0000000000..5f03faeb3b
--- /dev/null
+++ b/spaces/S000152/properties/P000090.md
@@ -0,0 +1,7 @@
+---
+space: S000152
+property: P000090
+value: true
+---
+
+By definition.
diff --git a/spaces/S000152/properties/P000181.md b/spaces/S000152/properties/P000181.md
new file mode 100644
index 0000000000..033a539268
--- /dev/null
+++ b/spaces/S000152/properties/P000181.md
@@ -0,0 +1,7 @@
+---
+space: S000152
+property: P000181
+value: true
+---
+
+By construction.
diff --git a/spaces/S000152/properties/P000202.md b/spaces/S000152/properties/P000202.md
new file mode 100644
index 0000000000..08c53915fb
--- /dev/null
+++ b/spaces/S000152/properties/P000202.md
@@ -0,0 +1,12 @@
+---
+space: S000152
+property: P000202
+value: true
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?"
+---
+
+The point $-1$ is a focal point of $X$ as it is a minimum of the poset.
+
+See part 2 of {{mathse:5007860}}.
diff --git a/spaces/S000158/README.md b/spaces/S000158/README.md
index 5b4effb29e..bb4e1ea8e8 100644
--- a/spaces/S000158/README.md
+++ b/spaces/S000158/README.md
@@ -1,9 +1,9 @@
 ---
 uid: S000158
-name: Unit interval
+name: Unit interval $[0,1]$
 refs:
   - zb: "1052.54001"
     name: General Topology (Willard)
 ---
-The subspace \(I=[0,1]=\{t\in \mathbb R : 0\leq x \leq 1\}\) of the
-Euclidean real line \(\mathbb{R}\).
+
+The subspace $I=[0,1]=\{t\in \mathbb R : 0\leq x \leq 1\}$ of {S25} $\mathbb{R}$.
diff --git a/spaces/S000159/README.md b/spaces/S000159/README.md
new file mode 100644
index 0000000000..71e7fbae39
--- /dev/null
+++ b/spaces/S000159/README.md
@@ -0,0 +1,11 @@
+---
+uid: S000159
+name: Right "open-ray" topology on $[0,1]$
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?"
+---
+
+$X$ has underlying set $[0,1]$ and the open sets are exactly $X$ and $(a,1]$ for $0 \leq a \leq 1$.
+
+This space is used in part 3 of {{mathse:5007860}}.
\ No newline at end of file
diff --git a/spaces/S000159/properties/P000027.md b/spaces/S000159/properties/P000027.md
new file mode 100644
index 0000000000..7fb0f8d726
--- /dev/null
+++ b/spaces/S000159/properties/P000027.md
@@ -0,0 +1,7 @@
+---
+space: S000159
+property: P000027
+value: true
+---
+ 
+$X$ and the sets $(a,1]$ for rational $0 \leq a \leq 1$ form a basis for the topology.
diff --git a/spaces/S000159/properties/P000043.md b/spaces/S000159/properties/P000043.md
new file mode 100644
index 0000000000..2c9dd119dd
--- /dev/null
+++ b/spaces/S000159/properties/P000043.md
@@ -0,0 +1,9 @@
+---
+space: S000159
+property: P000043
+value: true
+---
+
+The topology on $X$ is coarser than that of {S158}, so the formal identity map from {S158} to
+{S159} restricts to an arc between any two given distinct points in $X$.
+Therefore, since all nonempty open sets in $X$ are order-convex, they are {P38}.
diff --git a/spaces/S000159/properties/P000073.md b/spaces/S000159/properties/P000073.md
new file mode 100644
index 0000000000..521c82d036
--- /dev/null
+++ b/spaces/S000159/properties/P000073.md
@@ -0,0 +1,10 @@
+---
+space: S000159
+property: P000073
+value: true
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?
+---
+ 
+See part 3 of {{mathse:5007860}}.
diff --git a/spaces/S000159/properties/P000075.md b/spaces/S000159/properties/P000075.md
new file mode 100644
index 0000000000..6c86c36b15
--- /dev/null
+++ b/spaces/S000159/properties/P000075.md
@@ -0,0 +1,10 @@
+---
+space: S000159
+property: P000075
+value: false
+refs:
+  - mathse: 5007860
+    name: Answer to "For a compact sober "highly non-$T_1$" space, how much "highly connectedness" is needed to imply it's a spectral space?
+---
+ 
+See part 3 of {{mathse:5007860}}.
diff --git a/spaces/S000159/properties/P000130.md b/spaces/S000159/properties/P000130.md
new file mode 100644
index 0000000000..0c9eeaef53
--- /dev/null
+++ b/spaces/S000159/properties/P000130.md
@@ -0,0 +1,9 @@
+---
+space: S000159
+property: P000130
+value: true
+---
+ 
+Given a point $x\in X$, every neighborhood of $x$ contains a neighborhood of $x$
+of the form $[a,1]$ for some $a\in[0,1)$.
+Any such set $[a,1]$ is {P202} with $a$ as focal point, hence {P16}.
diff --git a/spaces/S000159/properties/P000139.md b/spaces/S000159/properties/P000139.md
new file mode 100644
index 0000000000..0d46242d81
--- /dev/null
+++ b/spaces/S000159/properties/P000139.md
@@ -0,0 +1,7 @@
+---
+space: S000159
+property: P000139
+value: false
+---
+ 
+No open set is a singleton.
diff --git a/spaces/S000159/properties/P000196.md b/spaces/S000159/properties/P000196.md
new file mode 100644
index 0000000000..9f586b4ae9
--- /dev/null
+++ b/spaces/S000159/properties/P000196.md
@@ -0,0 +1,7 @@
+---
+space: S000159
+property: P000196
+value: true
+---
+ 
+By construction.
diff --git a/spaces/S000159/properties/P000202.md b/spaces/S000159/properties/P000202.md
new file mode 100644
index 0000000000..cf13321b2a
--- /dev/null
+++ b/spaces/S000159/properties/P000202.md
@@ -0,0 +1,7 @@
+---
+space: S000159
+property: P000202
+value: true
+---
+ 
+The only neighborhood of $0$ is $X$.
diff --git a/spaces/S000160/README.md b/spaces/S000160/README.md
new file mode 100644
index 0000000000..f8c402f2ba
--- /dev/null
+++ b/spaces/S000160/README.md
@@ -0,0 +1,6 @@
+---
+uid: S000160
+name: Right "open-ray" topology on $\omega+1$
+---
+
+$X$ has underlying set $\omega+1$. The open sets are exactly $X$ and $(a, \omega]$ for $a \in X$.
diff --git a/spaces/S000160/properties/P000073.md b/spaces/S000160/properties/P000073.md
new file mode 100644
index 0000000000..b163a35189
--- /dev/null
+++ b/spaces/S000160/properties/P000073.md
@@ -0,0 +1,7 @@
+---
+space: S000160
+property: P000073
+value: true
+---
+
+By construction, any nonempty closed set is of the form $[0,a]$ for $a \in X$, which has a unique generic point $a$.
diff --git a/spaces/S000160/properties/P000139.md b/spaces/S000160/properties/P000139.md
new file mode 100644
index 0000000000..48a0d35523
--- /dev/null
+++ b/spaces/S000160/properties/P000139.md
@@ -0,0 +1,7 @@
+---
+space: S000160
+property: P000139
+value: false
+---
+
+Easily seen from the construction that no open set is a singleton.
diff --git a/spaces/S000160/properties/P000181.md b/spaces/S000160/properties/P000181.md
new file mode 100644
index 0000000000..580d9d6d76
--- /dev/null
+++ b/spaces/S000160/properties/P000181.md
@@ -0,0 +1,7 @@
+---
+space: S000160
+property: P000181
+value: true
+---
+
+By construction.
diff --git a/spaces/S000160/properties/P000196.md b/spaces/S000160/properties/P000196.md
new file mode 100644
index 0000000000..7052420e31
--- /dev/null
+++ b/spaces/S000160/properties/P000196.md
@@ -0,0 +1,7 @@
+---
+space: S000160
+property: P000196
+value: true
+---
+
+By construction.
diff --git a/spaces/S000160/properties/P000208.md b/spaces/S000160/properties/P000208.md
new file mode 100644
index 0000000000..0e4de35ebc
--- /dev/null
+++ b/spaces/S000160/properties/P000208.md
@@ -0,0 +1,8 @@
+---
+space: S000160
+property: P000208
+value: true
+---
+
+Every nonempty open subset of $X$ is of the form $[a,\omega]$ for $a < \omega$. Any such $[a,\omega]$ is
+{P202} with $a$ as focal point, so it is {P16}.
diff --git a/spaces/S000187/properties/P000089.md b/spaces/S000187/properties/P000089.md
deleted file mode 100644
index ac8337a5fe..0000000000
--- a/spaces/S000187/properties/P000089.md
+++ /dev/null
@@ -1,14 +0,0 @@
----
-space: S000187
-property: P000089
-value: true
----
-
-Let $f:X\to X$ be continuous.
-
-If $2$ is in the range of $f$, then
-$f^\leftarrow[\{2\}]$ is non-empty and open, and thus contains $2$.
-
-If $2$ is not in the range of $f$, then consider
-$f\upharpoonright\{0,1\}$, where $\{0,1\}$ is the subspace {S10}.
-Then $f\upharpoonright\{0,1\}$ has a fixed point as {S10|P89}.
diff --git a/spaces/S000188/properties/P000126.md b/spaces/S000188/properties/P000126.md
deleted file mode 100644
index d62599d611..0000000000
--- a/spaces/S000188/properties/P000126.md
+++ /dev/null
@@ -1,8 +0,0 @@
----
-space: S000188
-property: P000126
-value: true
----
-
-{S10|P126}.
-Hence so is $X$, as the topological sum of a {P52} space and a {P126} space.
diff --git a/spaces/S001103/properties/P000164.md b/spaces/S001103/properties/P000164.md
index a2de2c8ab2..57055e578a 100644
--- a/spaces/S001103/properties/P000164.md
+++ b/spaces/S001103/properties/P000164.md
@@ -4,4 +4,4 @@ property: P000164
 value: true
 ---
 
-The space has cardinality $\omega^{2^\mathfrak{c}}$, which is below the first inaccessible cardinal and thus non-measurable.
+$|X| = \omega^{2^\mathfrak{c}}$ is smaller than every measurable cardinal.
diff --git a/theorems/T000394.md b/theorems/T000394.md
index 790ff574ff..6d530c5a11 100644
--- a/theorems/T000394.md
+++ b/theorems/T000394.md
@@ -2,15 +2,13 @@
 uid: T000394
 if:
   and:
-    - P000052: true
+    - P000053: true
     - P000162: true
 then:
   P000164: true
 refs:
-- zb: "0684.54001"
-  name: General Topology (Engelking, 1989)
-- doi: 10.1007/978-1-4615-7819-2
-  name: Rings of Continuous Functions (Gillman and Jerison)
+- mo: 469593
+  name: If $X$ is metrizable, then $X$ is realcompact iff $|X|$ is non-measurable
 ---
 
-See theorem 12.2 in {{doi:10.1007/978-1-4615-7819-2}} or exercise 3.11.D of {{zb:0684.54001}}.
+See {{mo:469593}}. In particular [this answer by K. P. Hart](https://mathoverflow.net/a/469610/150060).
diff --git a/theorems/T000447.md b/theorems/T000447.md
index 4fc1561ecd..892553dd6f 100644
--- a/theorems/T000447.md
+++ b/theorems/T000447.md
@@ -6,6 +6,5 @@ then:
   P000001: true
 ---
 
-If $X$ is a non-$T_0$ space, then there exist distinct points $x,y\in X$ which have the same open neighborhoods.
-Then any selfmap $f: X\rightarrow X$ that maps into the set $\\{x, y\\}$ is continuous as $f^{-1}(U)$ is either $X$ or $\varnothing$ for any open set $U\subseteq X$.
-We may then easily select such maps without fixed points by requiring that $f(x)=y$ and $f(y)=x$.
+Suppose $X$ is not {P1}, with two topologically indistinguishable points $a$ and $b$.
+Then the map $f:X\to X$ defined by $f(x)=a$ for $x\ne a$ and $f(a)=b$ is continuous and does not have a fixed point.
diff --git a/theorems/T000575.md b/theorems/T000575.md
index c3ddc32d58..0be5428dd9 100644
--- a/theorems/T000575.md
+++ b/theorems/T000575.md
@@ -4,15 +4,13 @@ if:
   P000203: true
 then:
   P000108: true
-refs:
-- doi: 10.1016/0166-8641(92)90123-H
-  name: Almost discrete SV-spaces (Henrikson, Wilson)
 ---
-First, any almost discrete space $X$ is {P13}: if $A$ and $B$ are disjoint closed sets, then at least one of them, say $A$, does not contain the nonisolated point. Then $A$ is clopen, and thus $A$ and $B$ are separated by open sets.
 
-Note also {T574}. {P146}, of course, implies {P30}. Thus, by {T453}, $X$ is fully normal,
-which in turn implies it is {P88}. (See {T214} and {T648}.)
+Let $X$ be almost discrete.  Every subspace of $X$ is either almost discrete or discrete.
+Thus every subspace of $X$ is {P146}:
+- For {P203} subspaces: {T574}.
+- For {P52} subspaces, [(Explore)](https://topology.pi-base.org/spaces?q=Discrete+%2B+%7EUltraparacompact).
 
-A subspace of an almost discrete space is either almost discrete or discrete and so is always {P88} [(Explore)](https://topology.pi-base.org/spaces?q=Discrete+%2B+not+Collectionwise+normal). Hence any almost discrete space is {P108}.
-
-See also Lemma 2.1(i) of {{doi:10.1016/0166-8641(92)90123-H}}.
+The result then follows, since every {P146} space is {P88}
+[(Explore)](https://topology.pi-base.org/spaces?q=Ultraparacompact+%2B+%7ECollectionwise+normal
+).
diff --git a/theorems/T000622.md b/theorems/T000622.md
index 46685c84d8..f3e74d9784 100644
--- a/theorems/T000622.md
+++ b/theorems/T000622.md
@@ -3,12 +3,16 @@ uid: T000622
 if:
   and:
   - P000040: true
-  - P000016: true
+  - P000193: true
   - P000137: false
 then:
   P000202: true
 ---
 
-Since $X$ is {P40}, the family of nonempty closed sets in $X$ has the finite intersection property.
-As $X$ is {P16}, that family has nonempty intersection.
-Any point in that intersection belongs to every nonempty closed set.
+Assume to the contrary that $X$ is not {P202}. The intersection of $\overline{\{x\}}$
+for all $x \in X$ coincides with the intersection of all nonempty closed sets, so it is the set of all focal points of $X$,
+whence empty by assumption. Thus, $\{\overline{\{x\}}^c: x \in X\}$ is an open cover of $X$. As $X$ is {P193}, there
+is an open cover $\{V_x\}_{x \in X}$ of $X$ s.t. $\overline{V_x} \subseteq \overline{\{x\}}^c$ for all $x$. Now, fix $x_0 \in X$.
+There exists $x \in X$ s.t. $x_0 \in V_x \subseteq \overline{V_x} \subseteq \overline{\{x\}}^c$.
+Then $\overline{V_x}$ and $\overline{\{x\}}$ are nonempty disjoint closed sets,
+which contradicts $X$ being {P40}.
diff --git a/theorems/T000680.md b/theorems/T000680.md
new file mode 100644
index 0000000000..0b43a8ea2b
--- /dev/null
+++ b/theorems/T000680.md
@@ -0,0 +1,15 @@
+---
+uid: T000680
+if:
+  and:
+  - P000023: true
+  - P000134: true
+  - P000137: false
+  
+then:
+  P000206: true
+---
+
+A space $X$ is {P206} if and only if the Kolmogorov quotient of $X$ is {P206}.
+
+The Kolmogorov quotient of $X$ is {P23}, {P3} and non-empty, so strongly Choquet [(Explore)](https://topology.pi-base.org/spaces?q=weakly+locally+compact+%2B+T_2+%2B+not+empty+%2B+not+strongly+choquet).
diff --git a/theorems/T000681.md b/theorems/T000681.md
new file mode 100644
index 0000000000..9d6b185516
--- /dev/null
+++ b/theorems/T000681.md
@@ -0,0 +1,12 @@
+---
+uid: T000681
+if:
+  P000146: true
+then:
+  P000034: true
+---
+
+Let $\mathcal V$ be an open cover of $X$.  Since $X$ is {P146},
+$\mathcal V$ has an open refinement $\mathcal U$ that is a partition of $X$.
+And since the members of $\mathcal U$ are pairwise disjoint,
+$\mathcal U$ is a star refinement of $\mathcal V$.
diff --git a/theorems/T000682.md b/theorems/T000682.md
new file mode 100644
index 0000000000..d3c25a44d8
--- /dev/null
+++ b/theorems/T000682.md
@@ -0,0 +1,16 @@
+---
+uid: T000682
+if:
+  and:
+  - P000208: true
+  - P000201: true
+  - P000001: true
+  
+then:
+  P000089: true
+refs:
+- mathse: 5014330
+  name: Noetherian spaces with a generic point have the fixed point property
+---
+
+See {{mathse:5014330}}.
diff --git a/theorems/T000683.md b/theorems/T000683.md
new file mode 100644
index 0000000000..a754338f6e
--- /dev/null
+++ b/theorems/T000683.md
@@ -0,0 +1,15 @@
+---
+uid: T000683
+if:
+  and:
+  - P000104: true
+  - P000203: true
+  
+then:
+  P000102: true
+refs:
+- mathse: 5013902
+  name: Answer to "Symmetrizability and Semimetrizability of one-point compactifications"
+---
+
+See {{mathse:5013902}}.