proposition: Corollary connected_subspace_empty {X : TopologicalSpace} : connected (@SubspaceTopology X Empty_set).
proof: Proof. apply connected_subsingleton. intros [? []]. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)