proposition: Lemma Prf_pb1_law4 : Pullback_law4 Fibred1_p Fibred1_q Pb1_diese.
proof: Proof. unfold Pullback_law4, Pullback_eq1, Pullback_eq2 in |- *; intros r t1 t2 H h H1 H2. unfold Pb1_diese in |- *. apply (Prf_limit2 l). unfold Limit_eq in |- *; simpl in |- *. intro x; elim x; simpl in |- *. apply Sym; exact H1. apply Trans with (h o Fibred1_p o FMor G F12). apply Comp_l; apply (Eq_cone (Limiting_cone l) F12). apply Trans with ((h o Fibred1_p) o FMor G F12). apply Ass. apply Comp_r. apply Sym; exact H1. apply Sym; exact H2. Qed.
imports: Limit PULB Pullbacks