theorem Th12: :: MIDSP_2:12

for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x being Element of G holds Double (- x) = - (Double x)