for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 is linearly-closed holds
for v, u being Vector of V st v in V1 & u in V1 holds
v - u in V1