for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v, w being Element of V holds
( - (v + w) = (- w) - v & - (w + (- v)) = v - w & - (v - w) = w + (- v) & - ((- v) - w) = w + v & u - (w + v) = (u - v) - w ) by Lm4, Lm5, RLVECT_1:27, RLVECT_1:30, RLVECT_1:33;