let C be Category; :: thesis: for a, b being Object of C holds Hom a,b = (a Hom ) /\ (Hom b)
let a, b be Object of C; :: thesis: Hom a,b = (a Hom ) /\ (Hom b)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (a Hom ) /\ (Hom b) c= Hom a,b

let x be set ; :: thesis: ( x in Hom a,b implies x in (a Hom ) /\ (Hom b) )
assume A1: x in Hom a,b ; :: thesis: x in (a Hom ) /\ (Hom b)
then reconsider f = x as Morphism of C ;
A2: dom f = a by A1, CAT_1:18;
A3: cod f = b by A1, CAT_1:18;
A4: f in a Hom by A2, Th24;
f in Hom b by A3, Th23;
hence x in (a Hom ) /\ (Hom b) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (a Hom ) /\ (Hom b) or x in Hom a,b )
assume A5: x in (a Hom ) /\ (Hom b) ; :: thesis: x in Hom a,b
then A6: x in a Hom by XBOOLE_0:def 4;
A7: x in Hom b by A5, XBOOLE_0:def 4;
reconsider f = x as Morphism of C by A5;
A8: dom f = a by A6, Th24;
cod f = b by A7, Th23;
hence x in Hom a,b by A8; :: thesis: verum