:: deftheorem Def7 defines SubMeet RMOD_3:def 7 :
for R being Ring
for V being RightMod of R
for b₃ being BinOp of (Submodules V) holds
( b₃ = SubMeet V iff for A1, A2 being Element of Submodules V
for W1, W2 being Submodule of V st A1 = W1 & A2 = W2 holds
b₃ . (A1,A2) = W1 /\ W2 );