for AG being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds
( AG is Uniquely_Two_Divisible_Group iff ( ( for a being Element of AG ex b being Element of AG st b + b = a ) & ( for a being Element of AG st a + a = 0. AG holds
a = 0. AG ) ) ) by Def1, VECTSP_1:def 18;