set X = the carrier of ADG;
set XX = [:the carrier of ADG,the carrier of ADG:];
defpred S₁[ set , set ] 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 set 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 a', b', c', d' being Element of the carrier of ADG such that
A3: ( [a,b] = [a',b'] & [c,d] = [c',d'] ) and
A4: a' # d' = b' # c' by A1;
( a = a' & b = b' & c = c' & d = d' ) by A3, ZFMISC_1:33;
hence a # d = b # c by A4; :: 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