let R be Ring; :: thesis: for V being strict LeftMod of R holds V in Submodules V
let V be strict LeftMod of R; :: thesis: V in Submodules V
(Omega). V in Submodules V by VECTSP_5:def 3;
hence V in Submodules V ; :: thesis: verum