proposition: Lemma quotient_projection_surjective' {A : Type} (R : relation A): surjective (quotient_projection R).
proof: Proof. intro. destruct (quotient_projection_surjective y). now exists x. Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)