for F being Ring
for V, W being VectSp of F
for X being Subset of V st V is Subspace of W holds
X is Subset of W