proposition: Lemma Prf_pb1_law1 : Pullback_law1 (FMor G F12) (FMor G F32) Fibred1_p Fibred1_q.
proof: Proof. unfold Pullback_law1, Pullback_eq1 in |- *. apply Trans with (Limiting_cone l P2). apply Sym. apply (Eq_cone (Limiting_cone l) F12). apply (Eq_cone (Limiting_cone l) F32). Qed.
imports: Limit PULB Pullbacks