theorem Th7: :: ALGSTR_2:7

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