theorem Th2: :: ALGSTR_2:2

for G being Abelian right-distributive doubleLoop
for a, b being Element of G holds a * (- b) = - (a * b)