Toronto + not hyperconnected + finite => has an isolated point (#1786)

Author: felixpernegger

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}.