defpred S₁[ set , set ] means $1 c= $2;
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & S₁[x,y] ) ) from RELAT_1:sch 1();
take R ; :: thesis: ( field R = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in R iff Y c= Z ) ) )
thus field R = X :: thesis: for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in R iff Y c= Z )

proof

thus for x being set st x in field R holds
x in X :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X c= field R

proof

let x be set ; :: thesis: ( x in field R implies x in X )

A2: now

assume x in dom R ; :: thesis: ( x in field R implies x in X )
then ex y being set st [x,y] in R by RELAT_1:def 4;
hence ( x in field R implies x in X ) by A1; :: thesis: verum

end;

A3: now

assume x in rng R ; :: thesis: ( x in field R implies x in X )
then ex y being set st [y,x] in R by RELAT_1:def 5;
hence ( x in field R implies x in X ) by A1; :: thesis: verum

end;

assume x in field R ; :: thesis: x in X
hence x in X by A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field R )
assume x in X ; :: thesis: x in field R
then [x,x] in R by A1;
hence x in field R by RELAT_1:15; :: thesis: verum

end;

let Y, Z be set ; :: thesis: ( Y in X & Z in X implies ( [Y,Z] in R iff Y c= Z ) )
assume A4: ( Y in X & Z in X ) ; :: thesis: ( [Y,Z] in R iff Y c= Z )
thus ( [Y,Z] in R implies Y c= Z ) by A1; :: thesis: ( Y c= Z implies [Y,Z] in R )
thus ( Y c= Z implies [Y,Z] in R ) by A1, A4; :: thesis: verum