defpred S₁[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & D1 c= D2 );
consider R being Relation such that
A1: for x, y being object 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 object 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 object ; :: thesis: ( x in field R implies x in X )

A2: now :: thesis: ( x in dom R & x in field R implies x in X )

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

end;

A3: now :: thesis: ( x in rng R & x in field R implies x in X )

assume x in rng R ; :: thesis: ( x in field R implies x in X )
then ex y being object st [y,x] in R by XTUPLE_0:def 13;
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 object ; :: 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 )

hereby :: thesis: ( Y c= Z implies [Y,Z] in R )

assume [Y,Z] in R ; :: thesis: Y c= Z
then S₁[Y,Z] by A1;
hence Y c= Z ; :: thesis: verum

end;

thus ( Y c= Z implies [Y,Z] in R ) by A1, A4; :: thesis: verum