diff --git a/spaces/S000195/README.md b/spaces/S000195/README.md
index 4043cf15fa..8aa2060547 100644
--- a/spaces/S000195/README.md
+++ b/spaces/S000195/README.md
@@ -8,4 +8,4 @@ refs:
     name: Answer to "Is there a first countable, $T_1$, weakly Lindelof, sequentially compact space which is not also compact?"
 ---
 
-The set $\omega_1$ with topology equal to the join of the cofinite topology and left ray topology in the [lattice of topologies](https://en.wikipedia.org/wiki/Lattice_of_topologies) on $\omega_1$. This topology is generated by the sets of the form $\alpha\setminus F=[0,\alpha)\setminus F$ for $\alpha<\omega_1$ and $F\subseteq\omega_1$ finite.
+The set $\omega_1$ with topology equal to the join of the cofinite topology and left ray topology in the [lattice of topologies](https://en.wikipedia.org/wiki/Lattice_of_topologies) on $\omega_1$. This topology is the coarsest topology finer than both the cofinite topology and the left ray topology. It is generated by the sets of the form $\alpha\setminus F=[0,\alpha)\setminus F$ for $\alpha<\omega_1$ and $F\subseteq\omega_1$ finite.
diff --git a/spaces/S000195/properties/P000002.md b/spaces/S000195/properties/P000002.md
deleted file mode 100644
index 5966cebd50..0000000000
--- a/spaces/S000195/properties/P000002.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000195
-property: P000002
-value: true
-refs:
-    - mathse: 4874321
-      name: Answer to "Is there a first countable, $T_1$, weakly Lindelof, sequentially compact space which is not also compact?"
----
-
-By construction finite sets are closed.
diff --git a/spaces/S000195/properties/P000016.md b/spaces/S000195/properties/P000016.md
deleted file mode 100644
index be4e15d2e7..0000000000
--- a/spaces/S000195/properties/P000016.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000195
-property: P000016
-value: false
-refs:
-    - mathse: 4874321
-      name: Answer to "Is there a first countable, $T_1$, weakly Lindelof, sequentially compact space which is not also compact?"
----
-
-$\{\alpha:\alpha<\omega_1\}$ is an open cover with no finite subcover.
diff --git a/spaces/S000195/properties/P000024.md b/spaces/S000195/properties/P000024.md
new file mode 100644
index 0000000000..f347bdade0
--- /dev/null
+++ b/spaces/S000195/properties/P000024.md
@@ -0,0 +1,14 @@
+---
+space: S000195
+property: P000024
+value: false
+---
+
+Let $U$ be a closed neighborhood of $\omega$, and let $\alpha \ge \omega$. We have that $U$ is cofinite in $[0, \omega)$ (meaning that $[0, \omega) \setminus U$ is finite).
+
+Then let $V$ be a neighborhood of $\alpha$. Then $V$ is also cofinite in $[0, \omega)$.
+So $U \cap V$ is cofinite in $[0, \omega)$, and therefore nonempty.
+This argument works for any neighborhood $V$, so every neighborhood of $\alpha$ intersects $U$. Since $U$ is closed, $\alpha \in U$.
+
+Since this holds for any $\alpha \ge \omega$, we have that $[\omega, \omega_1) \subseteq U$.
+Then $\{ [0, \alpha) : \alpha \in X \}$ is an open cover of $U$ without finite subcover, so $U$ is not compact.
diff --git a/spaces/S000195/properties/P000026.md b/spaces/S000195/properties/P000026.md
deleted file mode 100644
index fd2d35018d..0000000000
--- a/spaces/S000195/properties/P000026.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000195
-property: P000026
-value: true
-refs:
-    - mathse: 4874321
-      name: Answer to "Is there a first countable, $T_1$, weakly Lindelof, sequentially compact space which is not also compact?"
----
-
-$\omega$ is a countable dense subset.
diff --git a/spaces/S000195/properties/P000084.md b/spaces/S000195/properties/P000084.md
new file mode 100644
index 0000000000..35e7772ff1
--- /dev/null
+++ b/spaces/S000195/properties/P000084.md
@@ -0,0 +1,7 @@
+---
+space: S000195
+property: P000084
+value: false
+---
+
+The point $\omega + \omega$ has no Hausdorff neighborhood.
diff --git a/spaces/S000195/properties/P000085.md b/spaces/S000195/properties/P000085.md
new file mode 100644
index 0000000000..98a1d761d4
--- /dev/null
+++ b/spaces/S000195/properties/P000085.md
@@ -0,0 +1,16 @@
+---
+space: S000195
+property: P000085
+value: false
+---
+
+Define a function $f : X \to \mathbb{R}$ by
+$$f(x)=
+\begin{cases}
+1/x &\text{if }x < \omega \text{ odd},\\
+0 &\text{if }x < \omega \text{ even},\\
+0 & \text{if }x \ge \omega
+\end{cases}
+$$
+
+Then $f$ is continuous, and $U = \{ x : f(x) \ne 0 \}$ and $V = \{ x : f(1 + x) \ne 0 \}$ are disjoint cozero sets whose closures both contain the point $\omega$.
diff --git a/spaces/S000195/properties/P000093.md b/spaces/S000195/properties/P000093.md
new file mode 100644
index 0000000000..d14279401c
--- /dev/null
+++ b/spaces/S000195/properties/P000093.md
@@ -0,0 +1,7 @@
+---
+space: S000195
+property: P000093
+value: true
+---
+
+For $\alpha < \omega_1$ and $F \subseteq \omega_1$ finite, let $U_{\alpha, F} = [0, \alpha) \setminus F$. Then the $U_{\alpha, F}$ are all countable and form a basis for the topology.
diff --git a/spaces/S000195/properties/P000099.md b/spaces/S000195/properties/P000099.md
deleted file mode 100644
index 0919b6be9a..0000000000
--- a/spaces/S000195/properties/P000099.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000195
-property: P000099
-value: false
----
-
-The sequence $a_n=n$ converges to every $\alpha\in\omega_1\setminus\omega$.
diff --git a/spaces/S000195/properties/P000101.md b/spaces/S000195/properties/P000101.md
new file mode 100644
index 0000000000..90e233d229
--- /dev/null
+++ b/spaces/S000195/properties/P000101.md
@@ -0,0 +1,15 @@
+---
+space: S000195
+property: P000101
+value: false
+---
+
+Define $p : X \to \mathbb{N}$ by $p(\alpha) = n$ if $\alpha = \beta + n$ but $\alpha \ne \gamma + n + 1$ for any ordinal $\gamma$.
+Define a function $f : X \to X$ by
+$$f(x)=
+\begin{cases}
+x &\text{if }p(x) \text{ even},\\
+x + 1 &\text{if }p(x) \text{ odd},\\
+\end{cases}
+$$
+Then $f$ is a retract onto $\{ 2 * x : x \in X \}$, which is not closed.
diff --git a/spaces/S000195/properties/P000115.md b/spaces/S000195/properties/P000115.md
new file mode 100644
index 0000000000..b69a8198b5
--- /dev/null
+++ b/spaces/S000195/properties/P000115.md
@@ -0,0 +1,16 @@
+---
+space: S000195
+property: P000115
+value: false
+---
+
+Consider the open cover $\mathcal{U} = \{ [0, \alpha) : \alpha < \omega_1 \}$. Suppose that $\mathcal{V}$ is a $\sigma$-locally finite closed refinement of $\mathcal{U}$.
+Since infinite closed subset of $X$ are unbounded, they are not subordinate to any of the $[0, \alpha) \in \mathcal{U}$, so $\mathcal{V}$ consists of finite subsets of $X$.
+Write $\mathcal{V} = \bigcup_n \mathcal{V}_n$, where $\mathcal{V}_n$ are locally finite.
+
+Suppose for sake of contradiction that $S = \bigcup\mathcal{V}_n$ is infinite. Since {S195|P21}, $S$ has a limit point.
+Call this limit point $x$, so $x$ is a limit point of $S$. Then $x$ has an open neighborhood $U$ intersecting only finitely many members of $\mathcal{V}_n$.
+All the members of $\mathcal{V}_n$ are finite, so $U \cap S$ is also finite. But {S195|P2} means that $U \cap S$ then has no limit points,
+so in particular $x$ is not a limit point of $U \cap S$.
+
+Then all the $\bigcup\mathcal{V}_n$ are finite, and so $X = \bigcup_n \bigcup\mathcal{V}_n$ is countable, which is impossible since $X$ is uncountable.
diff --git a/spaces/S000195/properties/P000130.md b/spaces/S000195/properties/P000130.md
new file mode 100644
index 0000000000..196c63eeb2
--- /dev/null
+++ b/spaces/S000195/properties/P000130.md
@@ -0,0 +1,8 @@
+---
+space: S000195
+property: P000130
+value: true
+---
+
+For $\alpha < \omega_1$ and $F \subseteq \omega_1$ finite, let $U_{\alpha, F} = [0, \alpha) \setminus F$.
+For a point $\alpha \in X$, sets of the form $U_{\alpha, F}$ for $\alpha \notin F$ are compact and form a neighborhood basis around $\alpha$.
diff --git a/spaces/S000195/properties/P000132.md b/spaces/S000195/properties/P000132.md
new file mode 100644
index 0000000000..2940d3c746
--- /dev/null
+++ b/spaces/S000195/properties/P000132.md
@@ -0,0 +1,9 @@
+---
+space: S000195
+property: P000132
+value: true
+---
+
+Every closed set is either finite or cocountable. Cocountable sets are $G_\delta$ because they are the countable intersection of complements of singletons. Since a finite union of $G_\delta$ sets is $G_\delta$, it suffices to check that singletons are $G_\delta$.
+
+Let $x \in X$, we need to show that $\{x\}$ is a countable intersection of open sets. For each $y < x$, the set $U_y = [0, x] \setminus \{y\}$ is open. There are only countably many $y < x$, so $\bigcap_{y < x} U_y = \{x\}$ is a $G_\delta$ set.
diff --git a/spaces/S000195/properties/P000142.md b/spaces/S000195/properties/P000142.md
new file mode 100644
index 0000000000..d50920bbd6
--- /dev/null
+++ b/spaces/S000195/properties/P000142.md
@@ -0,0 +1,18 @@
+---
+space: S000195
+property: P000142
+value: true
+---
+
+Let $A \subseteq X$ such that for every compact Hausdorff subspace $K \subseteq X$, the set $A \cap K$ is relatively closed in $K$.
+If $A$ is finite, then $X \setminus A = \bigcup_{\alpha < \omega_1} [0, \alpha) \setminus A$ is open.
+If $A$ is infinite, then being a subset of an ordinal, it is well-ordered, so it has an initial segment order-isomorphic to $\omega$.
+Let $U \subseteq A$ be this initial segment, and let $u$ be its supremum in $X$.
+
+Consider an arbitrary $v \in [u, \omega_1)$.
+Set $U_v = U \cup \{v\}$. Then $U_v$ with the subspace topology from $X$ is homeomorphic to {S20}.
+Then since {S20|P16} and {S20|P3}, the intersection $A \cap U_v$ is closed in $U_v$.
+Therefore $v \in A$. Since this works for any $v \in [u, \omega_1)$, we must have $[u, \omega_1) \subseteq A$.
+
+But also $A$ is disjoint from $[0, u) \setminus U$, since $U$ is an initial segment in $A$.
+We conclude that $A = U \cup [u, \omega_1)$. Then $X \setminus A = \bigcup_{\alpha < u} [0, \alpha) \setminus U$ is open (since each of the $[0, \alpha) \cap U$ is finite).
diff --git a/spaces/S000195/properties/P000169.md b/spaces/S000195/properties/P000169.md
new file mode 100644
index 0000000000..cd09fbcf17
--- /dev/null
+++ b/spaces/S000195/properties/P000169.md
@@ -0,0 +1,17 @@
+---
+space: S000195
+property: P000169
+value: false
+---
+
+Let $U$ be a regular open neighborhood of $\omega$, and let $\alpha \ge \omega$. We have that $U$ is cofinite in $[0, \omega)$ (meaning that $[0, \omega) \setminus U$ is finite).
+
+Then let $V$ be a neighborhood of $\alpha$. Then $V$ is also cofinite in $[0, \omega)$.
+So $U \cap V$ is cofinite in $[0, \omega)$, and therefore nonempty.
+This argument works for any neighborhood $V$, so every neighborhood of $\alpha$ intersects $U$. Therefore, $\alpha \in \operatorname{cl}(U)$.
+
+Since this holds for any $\alpha \ge \omega$, we have that $[\omega, \omega_1) \subseteq \operatorname{cl}(U)$.
+Then $X \setminus \operatorname{cl}(U)$ is a finite subset of $[0, \omega)$, so $\operatorname{cl}(U)$ is open.
+Then $\operatorname{int}(\operatorname{cl}(U)) = \operatorname{cl}(U)$.
+Since $U$ is regular we also have that $\operatorname{int}(\operatorname{cl}(U)) = U$, so in fact $\operatorname{cl}(U) = U$, and $[\omega, \omega_1) \subseteq U$.
+So no regular open neighborhood of $U$ misses any $\alpha \in [\omega, \omega_1)$.
diff --git a/spaces/S000195/properties/P000180.md b/spaces/S000195/properties/P000180.md
new file mode 100644
index 0000000000..132667ed67
--- /dev/null
+++ b/spaces/S000195/properties/P000180.md
@@ -0,0 +1,7 @@
+---
+space: S000195
+property: P000180
+value: true
+---
+
+Let $U \subseteq X$. Let $S$ be the set of $x \in U$ such that $[0, x) \cap U$ is finite. Then $S$ is a countable dense subset of $U$.