:: deftheorem Def2 defines /\ RMOD_3:def 2 :
for R being Ring
for V being RightMod of R
for W1, W2 being Submodule of V
for b₅ being strict Submodule of V holds
( b₅ = W1 /\ W2 iff the carrier of b₅ = the carrier of W1 /\ the carrier of W2 );