:: deftheorem Def15 defines Submodule FVALUAT1:def 15 :
for R being Ring
for P being RightIdeal of R
for b₃ being Submodule of RightModule R holds
( b₃ is Submodule of P iff the carrier of b₃ = P );