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 Th11;