for ADG being Uniquely_Two_Divisible_Group
for a, b, c, b9 being Element of ADG st a,b ==> b,c & a,b9 ==> b9,c holds
b = b9