let V be Z_Module; :: thesis: for W being Submodule of V holds (0). V is Submodule of W
let W be Submodule of V; :: thesis: (0). V is Submodule of W
the carrier of ((0). V) = {(0. V)} by Def10
.= {(0. W)} by Def9 ;
hence (0). V is Submodule of W by Th43; :: thesis: verum