proposition: Corollary connected_subspace_singleton {X : TopologicalSpace} (x : X) : connected (SubspaceTopology (Singleton x)).
proof: Proof. apply connected_subsingleton. intros [? []] [? []]. reflexivity. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)