:: deftheorem Def3 defines (0). RMOD_2:def 3 :
for R being Ring
for V being RightMod of R
for b₃ being strict Submodule of V holds
( b₃ = (0). V iff the carrier of b₃ = {(0. V)} );