let R be Ring; :: thesis: for V being strict RightMod of R holds V in Submodules V
let V be strict RightMod of R; :: thesis: V in Submodules V
ex W9 being strict Submodule of V st the carrier of ((Omega). V) = the carrier of W9 ;
hence V in Submodules V by Def3; :: thesis: verum