fact: Definition hom_third_surjection : Homomorphism (A/Ψ) (A/Φ) := BuildHomomorphism def_third_surjection.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism