diff --git a/spaces/S000215/README.md b/spaces/S000215/README.md
new file mode 100644
index 0000000000..0304911504
--- /dev/null
+++ b/spaces/S000215/README.md
@@ -0,0 +1,11 @@
+---
+uid: S000215
+name: Mysior plane
+refs:
+  - zb: "1265.54111"
+    name: r-realcompact spaces (Bhattacharya, Lipika)
+---
+
+For $X = \mathbb{R}^2$ let $(x, y)\in X$ for $y\neq 0$ be isolated, and if $y = 0$ let $$U_n(x) = \{(x, y): |y| < 1/n\}\cup \{(x+y+1, y): 0 < y < 1/n\}\cup \{(x+y+\sqrt{2}, -y) : 0 < y < 1/n\}$$ be open neighbourhoods of $(x, 0)$.
+
+Defined as example 5 of {{zb:1265.54111}}.
diff --git a/spaces/S000215/properties/P000022.md b/spaces/S000215/properties/P000022.md
new file mode 100644
index 0000000000..7537efe4c5
--- /dev/null
+++ b/spaces/S000215/properties/P000022.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000022
+value: false
+---
+
+$U_1(x)$ is clopen and homeomorphic to {S133} and {S133|P22}.
diff --git a/spaces/S000215/properties/P000031.md b/spaces/S000215/properties/P000031.md
new file mode 100644
index 0000000000..5de623b69d
--- /dev/null
+++ b/spaces/S000215/properties/P000031.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000031
+value: true
+---
+
+If $\mathcal{U}$ is an open cover of $X$, for each $x\in \mathbb{R}$ pick $n(x)$ such that $U_{n(x)}(x)\subseteq U$ for some $U\in\mathcal{U}$. Let $\mathcal{V} = \{U_{n(x)}(x) : x\in \mathbb{R}\}\cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_{n(x)}(x)\}$, then $\mathcal{V}$ is an open refinement of $\mathcal{U}$, and any point of $X$ is contained in at most two elements of $\mathcal{V}$.
diff --git a/spaces/S000215/properties/P000050.md b/spaces/S000215/properties/P000050.md
new file mode 100644
index 0000000000..e562b9850c
--- /dev/null
+++ b/spaces/S000215/properties/P000050.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000050
+value: true
+---
+
+The neighbourhood basis $U_n(x)$ of $(x, 0)$ is clopen for each $x\in \mathbb{R}$. 
diff --git a/spaces/S000215/properties/P000051.md b/spaces/S000215/properties/P000051.md
new file mode 100644
index 0000000000..eaf6d0a090
--- /dev/null
+++ b/spaces/S000215/properties/P000051.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000051
+value: true
+---
+
+If $Y\subseteq X$ is non-empty then it either $(x, y)\in Y$ for some $y\neq 0$ so that $(x, y)$ is isolated point of $Y$, or $Y\subseteq \mathbb{R}\times \{0\}$ and since $U_n(x)\cap \mathbb{R}\times \{0\} = \{(x, 0)\}$ it follows that $Y$ is discrete.
diff --git a/spaces/S000215/properties/P000061.md b/spaces/S000215/properties/P000061.md
new file mode 100644
index 0000000000..79fa7bd056
--- /dev/null
+++ b/spaces/S000215/properties/P000061.md
@@ -0,0 +1,12 @@
+---
+space: S000215
+property: P000061
+value: true
+refs:
+  - mathse: 4718866
+    name: Mysior plane is not realcompact
+---
+
+The property {P6} was proven in {{mathse:4718866}}.
+
+Note that if $V\subseteq X\setminus (\mathbb{R}\times \{0\})$ then $V = \bigcup_n V_n$ where $V_n = V\cap (X\setminus \mathbb{R}\times (-\frac{1}{n}, \frac{1}{n}))$ and $V_n$ are clopen, so that $U$ is a cozero set. If now $U\subseteq X$, let $V = X\setminus (U\cup \mathbb{R}\times \{0\})$, then $V$ is a cozero set and $V\cup U$ contains $X\setminus (\mathbb{R}\times \{0\})$ which is dense in $X$, so that $U\cup V$ is dense in $X$.
diff --git a/spaces/S000215/properties/P000062.md b/spaces/S000215/properties/P000062.md
new file mode 100644
index 0000000000..a6e29d534b
--- /dev/null
+++ b/spaces/S000215/properties/P000062.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000062
+value: false
+---
+
+The open cover $\mathcal{U} = \{\mathbb{R}\times (-1, 1)\}\cup \{\{x\} : x\in X\setminus (\mathbb{R}\times (-1, 1))\}$ is a partition, and if there is a subfamily $\mathcal{V}\subseteq \mathcal{U}$ such that $\bigcup \mathcal{V}$ is dense, then $\mathcal{V} = \mathcal{U}$. Since $\mathcal{U}$ is uncountable, $X$ is not {P62}.
diff --git a/spaces/S000215/properties/P000063.md b/spaces/S000215/properties/P000063.md
new file mode 100644
index 0000000000..7c485fbe6c
--- /dev/null
+++ b/spaces/S000215/properties/P000063.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000063
+value: true
+---
+
+Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$.
diff --git a/spaces/S000215/properties/P000065.md b/spaces/S000215/properties/P000065.md
new file mode 100644
index 0000000000..b894db47a6
--- /dev/null
+++ b/spaces/S000215/properties/P000065.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000065
+value: true
+---
+
+By definition.
diff --git a/spaces/S000215/properties/P000093.md b/spaces/S000215/properties/P000093.md
new file mode 100644
index 0000000000..11b75574dd
--- /dev/null
+++ b/spaces/S000215/properties/P000093.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000093
+value: false
+---
+
+$U_n(x)$ is homeomorphic to {S133} and {S133|P57}.
diff --git a/spaces/S000215/properties/P000105.md b/spaces/S000215/properties/P000105.md
new file mode 100644
index 0000000000..18db3b7851
--- /dev/null
+++ b/spaces/S000215/properties/P000105.md
@@ -0,0 +1,10 @@
+---
+space: S000215
+property: P000105
+value: false
+refs:
+  - mathse: 412625
+    name: Answer to "Every bounded non countable subset of $\mathbb{R}$ has a two-sided accumulation point."
+---
+
+Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a point $x$ of $C$ such that for any $y < x < z$ the sets $(y, x)\cap C$ and $(x, z)\cap C$ are uncountable (see {{mathse:412625}} for proof that such point exists), and $m$ such that $U_m(x)$ intersects countably many $U_n(y)$ for $y\in C$. Note that there is $z < x$ such that $U_n(y)\cap U_m(x)\neq \emptyset$ for all $y\in (z, x)\cap C$, and since $(z, x)\cap C$ is uncountable we obtain a contradiction.
diff --git a/spaces/S000215/properties/P000110.md b/spaces/S000215/properties/P000110.md
new file mode 100644
index 0000000000..b09510bc0c
--- /dev/null
+++ b/spaces/S000215/properties/P000110.md
@@ -0,0 +1,14 @@
+---
+space: S000215
+property: P000110
+value: true
+refs:
+  - doi: 10.2991/978-94-6239-216-8
+    name: Generalized Metric Spaces and Mappings (S. Lin, Z. Yun)
+---
+
+By theorem 1.2.13 of {{doi:10.2991/978-94-6239-216-8}} it suffices to show that $X$ is quasi-developable and a {P132}. 
+
+If $A\subseteq X$, write $A = A_0\cup A_1$ where $A_0\subseteq \mathbb{R}\times \{0\}$ and $A_1\subseteq \mathbb{R}\times (\mathbb{R}\setminus \{0\})$. Then $A_1$ is open and $A_0 = \bigcap_n \bigcup_{x\in A_0} U_n(x)$ so that $A$ is a union of two $G_\delta$-sets, and so $G_\delta$ itself, showing that any subset of $X$ is a $G_\delta$-set. In particular $X$ is a {P132}.
+
+To show $X$ is quasi-developable, let $\mathcal{V} = \{\{x\} : x\in X\setminus (\mathbb{R}\times \{0\})\}$ and $\mathcal{A}_n^i = \{U_n(x) : x\in [3m+i, 3m+i+1), m\in\mathbb{N}\}$ where $i = 0, 1, 2$. Then $\{\mathcal{V}\}\cup \{\mathcal{A}_n^i : n\in\mathbb{N}, i = 0, 1, 2\}$ is a quasi-development for $X$.
diff --git a/spaces/S000215/properties/P000120.md b/spaces/S000215/properties/P000120.md
new file mode 100644
index 0000000000..73ed97c5c6
--- /dev/null
+++ b/spaces/S000215/properties/P000120.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000120
+value: true
+---
+
+$U_1(x)$ is homeomorphic to {S133} and {S133|P133}.
diff --git a/spaces/S000215/properties/P000130.md b/spaces/S000215/properties/P000130.md
new file mode 100644
index 0000000000..0b1f8e4e4a
--- /dev/null
+++ b/spaces/S000215/properties/P000130.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000130
+value: false
+---
+
+$U_n(x)$ is homeomorphic to {S133} and {S133|P130}
diff --git a/spaces/S000215/properties/P000162.md b/spaces/S000215/properties/P000162.md
new file mode 100644
index 0000000000..e592b0d950
--- /dev/null
+++ b/spaces/S000215/properties/P000162.md
@@ -0,0 +1,10 @@
+---
+space: S000215
+property: P000162
+value: false
+refs:
+  - mathse: 4718866
+    name: Mysior plane is not realcompact
+---
+
+Proved in {{mathse:4718866}}.
diff --git a/spaces/S000215/properties/P000198.md b/spaces/S000215/properties/P000198.md
new file mode 100644
index 0000000000..2d7e5b5688
--- /dev/null
+++ b/spaces/S000215/properties/P000198.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000198
+value: false
+---
+
+$\mathbb{R}\times \{0\}$ is an uncountable closed discrete subset of $X$