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