theorem :: ZMODUL01:79
for R being Ring
for V being LeftMod of R
for W being Submodule of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W ) by VECTSP_4:69;