theorem Th143: :: ZMODUL01:143

for R being Ring
for V being LeftMod of R holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is Lattice by VECTSP_5:57;