let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, b, c, d being Element of ADG holds
( a,b ==> c,d iff a # d = b # c )
let a, b, c, d be Element of ADG; :: thesis: ( a,b ==> c,d iff a # d = b # c )
A1: the CONGR of (AV ADG) = CONGRD ADG ;

A2: now

assume a,b ==> c,d ; :: thesis: a # d = b # c
then [[a,b],[c,d]] in CONGRD ADG by A1, Def6;
hence a # d = b # c by Def4; :: thesis: verum

end;

now

assume a # d = b # c ; :: thesis: a,b ==> c,d
then [[a,b],[c,d]] in the CONGR of (AV ADG) by Def4;
hence a,b ==> c,d by Def6; :: thesis: verum

end;

hence ( a,b ==> c,d iff a # d = b # c ) by A2; :: thesis: verum