fact: Definition connected (X:TopologicalSpace) : Prop := forall S:Ensemble X, clopen S -> S = Empty_set \/ S = Full_set.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)