proposition: Corollary id_third_isomorphism : A/Ψ/Θ = A/Φ.
proof: Proof. exact (id_isomorphic isomorphic_third_isomorphism). Defined.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism