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
consider W' being strict Submodule of V such that
A1: the carrier of ((Omega). V) = the carrier of W' ;
thus V in Submodules V by A1, Def3; :: thesis: verum