theorem Th5: :: RLVECT_1:5

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( v + (- v) = 0. V & (- v) + v = 0. V )