let C be Category; :: thesis: ( C is Categorial implies C is with_triple-like_morphisms )
assume A1: C is Categorial ; :: thesis: C is with_triple-like_morphisms
then A2: ( the carrier of C is categorial & ( for m being Morphism of C
for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] ) ) by Def6;
let f be Morphism of C; :: according to CAT_5:def 1 :: thesis: ex x being set st f = [[(dom f),(cod f)],x]
reconsider A = dom f, B = cod f as Category by A2, Def5;
ex F being Functor of A,B st f = [[A,B],F] by A1, Def6;
hence ex x being set st f = [[(dom f),(cod f)],x] ; :: thesis: verum