take C = 1Cat (0,[[0,0],1]); :: thesis: C is with_triple-like_morphisms
let f be Morphism of C; :: according to CAT_5:def 1 :: thesis: ex x being set st f = [[(dom f),(cod f)],x]
take 1 ; :: thesis: f = [[(dom f),(cod f)],1]
dom f = 0 by TARSKI:def 1;
hence f = [[(dom f),(cod f)],1] by TARSKI:def 1; :: thesis: verum