theorem Th144: :: ZMODUL01:144

for V being Z_Module holds LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) is lower-bounded by VECTSP_5:58;