for ADG being Uniquely_Two_Divisible_Group
for a, b, c, d being Element of ADG holds
( a,b ==> c,d iff a # d = b # c ) by Def2;