diff --git a/theorems/T000898.md b/theorems/T000898.md new file mode 100644 index 000000000..a6740854f --- /dev/null +++ b/theorems/T000898.md @@ -0,0 +1,16 @@ +--- +uid: T000898 +if: + and: + - P000219: true + - P000039 : false + - P000078: false +then: + P000139: true +--- + +Since $X$ is not {P39}, there is a nonempty open set $U$ which is not dense. Let $x_0 \in U$ and $x_1 \in X\setminus \overline{U}$. + +Since $X$ is infinite, we either have $|U \cup \{x_1\}| = |X|$ or $|(X \setminus U) \cup \{x_0\}| = |X|$. + +Both $U \cup \{x_1\}$ and $(X \setminus U) \cup \{x_0\}$ contain an isolated point, thus the assertion follows by {P219}.