let V be strict Z_Module; :: thesis: V in Submodules V
(Omega). V in Submodules V by VECTSP_5:def 3;
hence V in Submodules V ; :: thesis: verum