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