for V, W being Z_Module
for X being Subset of V st V is Submodule of W holds
X is Subset of W