Theorem T000649

Door ∧ ¬Empty ⇒ Has a closed point

If a Door space has no closed points, then every singleton is open, which implies that the space is Discrete. This is a contradiction if the space is non-empty.

The converse ( Has a closed point ⇒ Door ∧ ¬Empty ) cannot be proven from other theorems or disproven from a counterexample.

You can learn how to contribute a theorem or counterexample here.