for ADG being Uniquely_Two_Divisible_Group
for a, b, c being Element of ADG ex d being Element of ADG st a,b ==> c,d