for K being Ring
for V being LeftMod of K
for W, W1, W2 being Subspace of V holds
( (0). W c= V & (0). V c= W & (0). W1 c= W2 ) by VECTSP_4:38, VECTSP_4:39, VECTSP_4:40;