defpred S1[ 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 & S1[x,y] ) ) from 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 ; :: 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 S1[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