theorem :: RLVECT_1:28

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