let A be Category; :: thesis: for a, b, c, d being Object of A st Hom a,b meets Hom c,d holds
( a = c & b = d )
let a, b, c, d be Object of A; :: thesis: ( Hom a,b meets Hom c,d implies ( a = c & b = d ) )
assume Hom a,b meets Hom c,d ; :: thesis: ( a = c & b = d )
then consider x being set such that
A1: ( x in Hom a,b & x in Hom c,d ) by XBOOLE_0:3;
reconsider x = x as Morphism of A by A1;
( dom x = a & cod x = b & dom x = c & cod x = d ) by A1, CAT_1:18;
hence ( a = c & b = d ) ; :: thesis: verum