defpred S_{1}[ 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_{1}[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 )

assume A4: ( Y in X & Z in X ) ; :: thesis: ( [Y,Z] in R iff Y c= Z )

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

( 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

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

let Y, Z be set ; :: thesis: ( Y in X & Z in X implies ( [Y,Z] in R iff Y c= Z ) )
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

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;x in X :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X c= field R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field R )
let x be object ; :: thesis: ( x in field R implies x in X )

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

end;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;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

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

assume
x in field R
; :: thesis: x in Xassume
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;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

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

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

assume A4: ( Y in X & Z in X ) ; :: thesis: ( [Y,Z] in R iff Y c= Z )

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