theorem Th49: :: RMOD_3:49

for R being Ring
for V being RightMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is 1_Lattice