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