proposition: Lemma Thl_mu_cone_law : Cone_law Thl_mu_tau.
proof: Proof. unfold Cone_law in |- *; intros j k u; unfold Thl_mu_tau in |- *. apply Trans with (Thl_e o Thl_f o Proj1 Thl_l_Fu (Build_Arrs u)). apply Comp_l. apply (Thl_diag1 (Build_Arrs u)). apply Trans with (Thl_e o Proj1 Thl_l_Fi j o FMor F u). apply Trans with (Thl_e o Thl_g o Proj1 Thl_l_Fu (Build_Arrs u)). apply Trans with ((Thl_e o Thl_f) o Proj1 Thl_l_Fu (Build_Arrs u)). apply Ass. apply Trans with ((Thl_e o Thl_g) o Proj1 Thl_l_Fu (Build_Arrs u)). apply Comp_r. apply (Prf_E1_law1 Thl_l_fg Elt1 Elt2). apply Ass1. apply Comp_l. apply Sym. exact (Thl_diag2 (Build_Arrs u)). apply Ass. Qed.
imports: Equalizers1 Products1