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 object such that
A1: x in Hom (a,b) and
A2: x in Hom (c,d) by XBOOLE_0:3;
reconsider x = x as Morphism of A by A1;
A3: cod x = b by A1, CAT_1:1;
dom x = a by A1, CAT_1:1;
hence ( a = c & b = d ) by A2, A3, CAT_1:1; :: thesis: verum