theorem :: RLVECT_4:1

for V being RealLinearSpace
for v, w being VECTOR of V holds
( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w )