set X = the carrier of ADG;
set XX = [: the carrier of ADG, the carrier of ADG:];
let P, Q be Relation of [: the carrier of ADG, the carrier of ADG:]; :: thesis: ( ( for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in P iff a # d = b # c ) ) & ( for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in Q iff a # d = b # c ) ) implies P = Q )
assume that
A7: for a, b, c, d being Element of the carrier of ADG holds
( [[a,b],[c,d]] in P iff a # d = b # c ) and
A8: for a, b, c, d being Element of the carrier of ADG holds
( [[a,b],[c,d]] in Q iff a # d = b # c ) ; :: thesis: P = Q
for x, y being object holds
( [x,y] in P iff [x,y] in Q )

proof

let x, y be object ; :: thesis: ( [x,y] in P iff [x,y] in Q )

A9: now :: thesis: ( [x,y] in Q implies [x,y] in P )

assume A10: [x,y] in Q ; :: thesis: [x,y] in P
then x in [: the carrier of ADG, the carrier of ADG:] by ZFMISC_1:87;
then consider a, b being Element of ADG such that
A11: x = [a,b] by DOMAIN_1:1;
y in [: the carrier of ADG, the carrier of ADG:] by A10, ZFMISC_1:87;
then consider c, d being Element of ADG such that
A12: y = [c,d] by DOMAIN_1:1;
( [x,y] in Q iff a # d = b # c ) by A8, A11, A12;
hence [x,y] in P by A7, A10, A11, A12; :: thesis: verum

end;

now :: thesis: ( [x,y] in P implies [x,y] in Q )

assume A13: [x,y] in P ; :: thesis: [x,y] in Q
then x in [: the carrier of ADG, the carrier of ADG:] by ZFMISC_1:87;
then consider a, b being Element of ADG such that
A14: x = [a,b] by DOMAIN_1:1;
y in [: the carrier of ADG, the carrier of ADG:] by A13, ZFMISC_1:87;
then consider c, d being Element of ADG such that
A15: y = [c,d] by DOMAIN_1:1;
( [x,y] in P iff a # d = b # c ) by A7, A14, A15;
hence [x,y] in Q by A8, A13, A14, A15; :: thesis: verum

end;

hence ( [x,y] in P iff [x,y] in Q ) by A9; :: thesis: verum

end;

hence P = Q by RELAT_1:def 2; :: thesis: verum