theorem Th60: :: RING_3:61
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R holds (- 1) '*' a = - a