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 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:18;
dom x = a by A1, CAT_1:18;
hence ( a = c & b = d ) by A2, A3, CAT_1:18; :: thesis: verum