theorem Th11: :: LMOD_7:11

for K being Ring
for V being LeftMod of K
for a1, a2 being Vector of V
for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W ) by VECTSP_4:55, Th10;