theorem :: RLVECT_1:31

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (v + w) = (- w) + (- v) by Lm3;