theorem Th3: :: VECTSP_2:3

for R being non empty right_complementable add-associative right_zeroed addLoopStr
for x being Element of R holds
( x = 0. R iff - x = 0. R )