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 )
proof
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;
assume A11: [x,y] in R2 ; :: thesis: [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