proposition: Theorem isomorphic_second_isomorphism : (A&&P) / Ψ ≅ (A/Φ) && Q.
proof: Proof. exact (BuildIsomorphic def_second_isomorphism). Defined.
imports: HSet Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra