proposition: Lemma Prf_pb1_law3 : Pullback_law3 Fibred1_q Pb1_diese.
proof: Proof. unfold Pullback_law3, Pullback_eq1, Pullback_eq2 in |- *; intros r t1 t2 H. apply Sym; apply (Prf_limit1 l (Pulb_cone H) P3). Qed.
imports: Limit PULB Pullbacks