for V being RealLinearSpace
for u, v, w, y being VECTOR of V st y + u = v + w holds
y - w = v - u