set IT = { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } ;
for x being object st x in { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } holds
x in [:(Ob C),(Ob C):]

proof

let x be object ; :: thesis: ( x in { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } implies x in [:(Ob C),(Ob C):] )
assume x in { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } ; :: thesis: x in [:(Ob C),(Ob C):]
then consider a, b being Object of C such that
A1: ( x = [a,b] & ex f being morphism of C st f in Hom (a,b) ) ;
not C is empty by A1;
hence x in [:(Ob C),(Ob C):] by A1, ZFMISC_1:def 2; :: thesis: verum

end;

hence { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } is Relation of (Ob C) by TARSKI:def 3; :: thesis: verum