theorem :: ZMODLAT2:27

for L being positive-definite Z_Lattice
for Z being non empty LatticeStr over INT.Ring st Z is finitely-generated Submodule of DivisibleMod L & the scalar of Z = (ScProductDM L) || the carrier of Z holds
Z is Z_Lattice by ThSLX2;