let V be Z_Module; :: thesis: for W1, W2 being Submodule of V holds W1 is Submodule of W1 + W2
let W1, W2 be Submodule of V; :: thesis: W1 is Submodule of W1 + W2
the carrier of W1 c= the carrier of (W1 + W2) by Lm6;
hence W1 is Submodule of W1 + W2 by Th43; :: thesis: verum