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 ;
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;
ex F being Functor of A,B st f = [[A,B],F] by A1;
hence ex x being set st f = [[(dom f),(cod f)],x] ; :: thesis: verum