let R1, R2 be Relation; :: thesis: ( field R1 = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R1 iff Y c= Z ) ) & field R2 = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R2 iff Y c= Z ) ) implies R1 = R2 )

assume that

A5: field R1 = X and

A6: for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R1 iff Y c= Z ) and

A7: field R2 = X and

A8: for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R2 iff Y c= Z ) ; :: thesis: R1 = R2

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )

thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( not [x,y] in R2 or [x,y] in R1 )

then A12: ( x in field R2 & y in field R2 ) by RELAT_1:15;

reconsider x = x, y = y as set by TARSKI:1;

x c= y by A7, A8, A11, A12;

hence [x,y] in R1 by A6, A7, A12; :: thesis: verum

( [Y,Z] in R1 iff Y c= Z ) ) & field R2 = X & ( for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R2 iff Y c= Z ) ) implies R1 = R2 )

assume that

A5: field R1 = X and

A6: for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R1 iff Y c= Z ) and

A7: field R2 = X and

A8: for Y, Z being set st Y in X & Z in X holds

( [Y,Z] in R2 iff Y c= Z ) ; :: thesis: R1 = R2

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )

thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( not [x,y] in R2 or [x,y] in R1 )

proof

assume A11:
[x,y] in R2
; :: thesis: [x,y] in R1
assume A9:
[x,y] in R1
; :: thesis: [x,y] in R2

then A10: ( x in field R1 & y in field R1 ) by RELAT_1:15;

reconsider x = x, y = y as set by TARSKI:1;

x c= y by A5, A6, A9, A10;

hence [x,y] in R2 by A5, A8, A10; :: thesis: verum

end;then A10: ( x in field R1 & y in field R1 ) by RELAT_1:15;

reconsider x = x, y = y as set by TARSKI:1;

x c= y by A5, A6, A9, A10;

hence [x,y] in R2 by A5, A8, A10; :: thesis: verum

then A12: ( x in field R2 & y in field R2 ) by RELAT_1:15;

reconsider x = x, y = y as set by TARSKI:1;

x c= y by A7, A8, A11, A12;

hence [x,y] in R1 by A6, A7, A12; :: thesis: verum