set X = the carrier of ADG;
set XX = [: the carrier of ADG, the carrier of ADG:];
defpred S₁[ object , object ] means ex a, b, c, d being Element of the carrier of ADG st
( $1 = [a,b] & $2 = [c,d] & a # d = b # c );
consider P being Relation of [: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:] such that
A1: for x, y being object holds
( [x,y] in P iff ( x in [: the carrier of ADG, the carrier of ADG:] & y in [: the carrier of ADG, the carrier of ADG:] & S₁[x,y] ) ) from RELSET_1:sch 1();
take P ; :: thesis: for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in P iff a # d = b # c )
let a, b, c, d be Element of the carrier of ADG; :: thesis: ( [[a,b],[c,d]] in P iff a # d = b # c )
A2: ( [[a,b],[c,d]] in P implies a # d = b # c )

proof

assume [[a,b],[c,d]] in P ; :: thesis: a # d = b # c
then consider a9, b9, c9, d9 being Element of the carrier of ADG such that
A3: [a,b] = [a9,b9] and
A4: [c,d] = [c9,d9] and
A5: a9 # d9 = b9 # c9 by A1;
A6: c = c9 by A4, XTUPLE_0:1;
( a = a9 & b = b9 ) by A3, XTUPLE_0:1;
hence a # d = b # c by A4, A5, A6, XTUPLE_0:1; :: thesis: verum

end;

( [a,b] in [: the carrier of ADG, the carrier of ADG:] & [c,d] in [: the carrier of ADG, the carrier of ADG:] ) by ZFMISC_1:def 2;
hence ( [[a,b],[c,d]] in P iff a # d = b # c ) by A1, A2; :: thesis: verum