proposition: Lemma Comma_complete : forall (X A : Category) (G : Functor A X), Complete A -> Continuous G -> forall x : X, Complete (Comma G x).
proof: Proof. intros X A G cA cG x. unfold Complete in |- *; intros J F. exact (Comma_l_F1 (cA J) (cG J) F). Defined.
imports: Pres_Limits Comma_proj