theorem :: RLVECT_1:33
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds - (v - w) = w + (- v)