:: deftheorem Def3 defines Submodules RMOD_3:def 3 :
for R being Ring
for V being RightMod of R
for b₃ being set holds
( b₃ = Submodules V iff for x being object holds
( x in b₃ iff ex W being strict Submodule of V st W = x ) );