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):]

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

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
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;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