let V, W be Z_Module; :: thesis: for X being Subset of V st V is Submodule of W holds
X is Subset of W
let X be Subset of V; :: thesis: ( V is Submodule of W implies X is Subset of W )
assume V is Submodule of W ; :: thesis: X is Subset of W
then A1: [#] V c= [#] W by VECTSP_4:def 2;
X c= [#] W by A1;
hence X is Subset of W ; :: thesis: verum