proposition: Lemma FT_cd2_law : h =_S f i o FMor G t.
proof: Proof. apply Trans with (ApAphi la (Id (Adjoint la x) o t)). apply Trans with (ApAphi la t). apply Sym. exact (Idl_inv (NTa_areIso la (Build_POb1 x r)) h). apply AphiPres. apply Idl1. apply (Adj_eq3 la t (Id (Adjoint la x))). Defined.
imports: Limit Adj_UA Single FAFT_SSC2