ex ADG being Uniquely_Two_Divisible_Group ex a, b being Element of ADG st a <> b by Th6;