end;

defpred S₁[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
A6: for x being set st x in A holds
ex y being set st
( y in C & S₁[x,y] )

let x be set ; :: thesis:
assume A7: x in A ; :: thesis:
then reconsider x9 = x as Element of R ;
not the carrier of R is empty by A5;
then x9 in the carrier of R ;
then x9 in union C by EQREL_1:def 4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def 4;
take y ; :: thesis:
thus ( y in C & S₁[x,y] ) by A7, A8, A9; :: thesis:

end;

consider f being Function of A,C such that
A10: for x being set st x in A holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);
take f ; :: thesis:
A11: f is one-to-one

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A12: x1 in dom f and
A13: x2 in dom f and
A14: f . x1 = f . x2 ; :: thesis:
A15: x1 in f . x1 by A12, A10;
A16: x2 in f . x2 by A13, A10;
f . x1 in C by A5, A12, FUNCT_2:5;
then f . x1 is Clique of R by Def11;
hence x1 = x2 by A12, A13, A15, A16, A14, Th15; :: thesis:

end;

end;