set X = the carrier of ADG;
set XX = [: the carrier of ADG, the carrier of ADG:];
defpred S1[ 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:] & S1[x,y] ) )
from RELSET_1:sch 1();
take
P
; 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; ( [[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
;
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;
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; verum