theorem ThSLGM3: :: ZMODLAT3:52

for L being positive-definite Z_Lattice
for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
LX is positive-definite