proposition: Lemma Tc_limconeF_tau_com_law : forall i : J, Com_law (axf:=Tc_limF) (bxg:=F i) (Limiting_cone l_F' i).
proof: Proof. unfold Com_law in |- *; intro i. apply Sym; exact (Prf_limit1 l_GF' Tc_cone i). Qed.
imports: Pres_Limits Comma_proj