theorem :: LMOD_6:39

for K being Ring
for V being LeftMod of K
for W1, W2 being Subspace of V holds
( W1 c= W2 iff @ ([#] W1) c= @ ([#] W2) ) by Th38;