fact: Definition QuotientTopology {X : TopologicalSpace} (R : Relation X) : TopologicalSpace := StrongTopology (True_rect (quotient_projection R)).
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)