proposition: Lemma Tc_t_tau_cone_law : Cone_law (c:=Ob_com_ob axf) (F:=F') Tc_t_tau.
proof: Proof. unfold Cone_law in |- *; intros i j g. generalize (Eq_cone t g). intro H. apply Trans with (FMor (Comma_proj G x) (t i o FMor F g)). exact (Pres (FMap (Comma_proj G x) axf (F j)) H). exact (Prf_Fcomp_law (Comma_proj G x) (t i) (FMor F g)). Qed.
imports: Pres_Limits Comma_proj