defpred S₁[ set , set ] means ex Y, Z being set st
( $1 = Y & $2 = Z & Y c= Z );
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:30; :: 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 ) :: thesis: ( Y c= Z implies [Y,Z] in R )

proof

assume [Y,Z] in R ; :: thesis: Y c= Z
then ex V1, V2 being set st
( V1 = Y & V2 = Z & V1 c= V2 ) by A1;
hence Y c= Z ; :: thesis: verum

end;

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