theorem :: ZMODUL01:147

for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is modular by VECTSP_5:61;