proposition: Lemma FT_UA_law1 : UA_eq FT_tau_d h FT_h_diese.
proof: Proof. unfold UA_eq, FT_h_diese in |- *. apply Trans with (FT_tau_d o FMor G (FT_Apeps FT_i0) o FMor G FT_t). apply Comp_l; apply FComp. apply Trans with ((FT_tau_d o FMor G (FT_Apeps FT_i0)) o FMor G FT_t). apply Ass. apply Trans with (FT_tau FT_i0 o FMor G FT_t). apply Comp_r. apply Sym; apply (FT_eq_tau FT_i0). apply Sym; apply (Prf_SSC2_law (s x) h). Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1