for V being RealLinearSpace
for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M