end;

defpred S₁[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
P: 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 A1: x in A ; :: thesis:
then reconsider x9 = x as Element of R ;
not the carrier of R is empty by S1;
then x9 in the carrier of R ;
then x9 in union C by EQREL_1:def 6;
then consider y being set such that
B1: x in y and
C1: y in C by TARSKI:def 4;
take y ; :: thesis:
thus ( y in C & S₁[x,y] ) by A1, B1, C1; :: thesis:

end;

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

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A1: x1 in dom f and
B1: x2 in dom f and
C1: f . x1 = f . x2 ; :: thesis:
F1: x1 in f . x1 by A1, Q;
G1: x2 in f . x2 by B1, Q;
f . x1 in C by S1, A1, FUNCT_2:7;
then f . x1 is Clique of R by LCpart;
hence x1 = x2 by A1, B1, F1, G1, C1, ACClique; :: thesis:

end;

end;