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 ;
( dom f = a & cod f = b ) by A1, CAT_1:18;
then ( f in a Hom & f in Hom b ) by Th23, Th24;
hence x in (a Hom ) /\ (Hom b) by 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 A2: x in (a Hom ) /\ (Hom b) ; :: thesis: x in Hom a,b
then A3: ( x in a Hom & x in Hom b ) by XBOOLE_0:def 4;
reconsider f = x as Morphism of C by A2;
( dom f = a & cod f = b ) by A3, Th23, Th24;
hence x in Hom a,b ; :: thesis: verum